Z3
src
api
dotnet
core
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
33
public
class
ContractInvariantMethod
:
Attribute
34
{
35
public
ContractInvariantMethod
() { }
36
}
37
38
public
class
ContractVerification
:
Attribute
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
}
System.Diagnostics.Contracts.ContractInvariantMethod
Definition:
DummyContracts.cs:33
Attribute
System.Diagnostics.Contracts.ContractClassFor
Definition:
DummyContracts.cs:28
System.Diagnostics.Contracts.Pure
Definition:
DummyContracts.cs:43
System
System.Diagnostics.Contracts.ContractVerification.ContractVerification
ContractVerification(bool b)
Definition:
DummyContracts.cs:40
System.Diagnostics.Contracts.ContractVerification
Definition:
DummyContracts.cs:38
System.Diagnostics.Contracts.ContractClassFor.ContractClassFor
ContractClassFor(Type t)
Definition:
DummyContracts.cs:30
z3py.ForAll
def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Definition:
z3py.py:1876
System.Diagnostics.Contracts.ContractClass.ContractClass
ContractClass(Type t)
Definition:
DummyContracts.cs:25
System.Diagnostics.Contracts.ContractInvariantMethod.ContractInvariantMethod
ContractInvariantMethod()
Definition:
DummyContracts.cs:35
System.Diagnostics.Contracts.ContractClass
Definition:
DummyContracts.cs:23
Generated on Sat Nov 12 2016 23:18:40 for Z3 by
1.8.12