diff options
| author |  Rustan Leino <unknown> | 2013-02-20 17:38:56 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-02-20 17:38:56 -0800 |
| commit | d26d672bb7cfea66721d4a819477f3a7541d4631 (patch) | |
| tree | 490862b3b0f52367d217743752f07a88c72774ec /Source/Dafny/RefinementTransformer.cs | |
| parent | 5c5d0318c70d53eb8b287b07edfce96b6888a540 (diff) | |
Added Equals method on Type
Fixed some precondition violations
Various improvements in Contracts
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index e1070dad..a49b3b42 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -462,6 +462,7 @@ namespace Microsoft.Dafny moduleUnderConstruction = null;
}
Function CloneFunction(IToken tok, Function f, bool isGhost, List<Expression> moreEnsures, Expression moreBody, Expression replacementBody, bool checkPrevPostconditions, Attributes moreAttributes) {
+ Contract.Requires(tok != null);
Contract.Requires(moreBody == null || f is Predicate);
Contract.Requires(moreBody == null || replacementBody == null);
|