Z3
DummyContracts.cs
Go to the documentation of this file.
1 /*++
2 Copyright (<c>) 2016 Microsoft Corporation
3 
4 Module Name:
5 
6  Contracts.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Dummy Code Contracts class for .NET
11  frameworks that don't support them (e.g., CoreCLR).
12 
13 Author:
14 
15  Christoph Wintersteiger (cwinter) 2016-10-06
16 
17 Notes:
18 
19 --*/
20 
21 namespace System.Diagnostics.Contracts
22 {
23  public class ContractClass : Attribute
24  {
25  public ContractClass(Type t) { }
26  }
27 
28  public class ContractClassFor : Attribute
29  {
30  public ContractClassFor(Type t) { }
31  }
32 
34  {
36  }
37 
39  {
40  public ContractVerification(bool b) { }
41  }
42 
43  public class Pure : Attribute { }
44 
45  public static class Contract
46  {
47  public static void Ensures(bool b) { }
48  public static void Requires(bool b) { }
49  public static void Assume(bool b, string msg) { }
50  public static void Assert(bool b) { }
51  public static bool ForAll(bool b) { return true; }
52  public static bool ForAll(Object c, Func<Object, bool> p) { return true; }
53  public static bool ForAll(int from, int to, Predicate<int> p) { return true; }
54  public static void Invariant(bool b) { }
55  public static T[] Result<T>() { return new T[1]; }
56  public static void EndContractBlock() { }
57  public static T ValueAtReturn<T>(out T v) { T[] t = new T[1]; v = t[0]; return v; }
58  }
59 }
def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Definition: z3py.py:1876