diff options
| author |  tabarbe <unknown> | 2010-08-19 22:25:47 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-19 22:25:47 +0000 |
| commit | 569162aad309729152bf364aa26e630e1163229f (patch) | |
| tree | 32f9fe9ee525d7ccec5d2cd69188cdcde83d4e47 /Source | |
| parent | 73af19627afbb0f3185115abbc5ad183342234d4 (diff) | |
Boogie: Removed and completed a task comment
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 03a06672..a17cea23 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -548,14 +548,18 @@ void ObjectInvariant() public abstract ProverContext Context { get; }
public abstract VCExpressionGenerator VCExprGen { get; }
}
- public class ProverInterfaceContracts:ProverInterface{//TODO Contracts class
+ public class ProverInterfaceContracts:ProverInterface{
public override ProverContext Context {
get {
+ Contract.Ensures(Contract.Result<ProverContext>() != null);
+
throw new NotImplementedException();
}
}
public override VCExpressionGenerator VCExprGen {
get {
+ Contract.Ensures(Contract.Result<VCExpressionGenerator>() != null);
+
throw new NotImplementedException();
}
}
|