diff options
| author |  rustanleino <unknown> | 2010-10-22 01:34:13 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-10-22 01:34:13 +0000 |
| commit | 75affe5a214df74d2927785d666fbe3d7871e867 (patch) | |
| tree | 2c849dc5fea8ea7e0406ab03d9c622d47909bf9a /Chalice/refinements | |
| parent | 7b2e81b5f228e09feaedd215c7d2fc7eed0ffe1c (diff) | |
Miscellaneous changes:
* Also copy CodeContractExtender in PrepareBoogieZip.bat
* Added some comments and a new program in Test/textbook
* Included refinement keywords in Chalice emacs mode
* Used assignment instead of spec statement in DuplicatesVideo.chalice
Diffstat (limited to 'Chalice/refinements')
| -rw-r--r-- | Chalice/refinements/DuplicatesVideo.chalice | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Chalice/refinements/DuplicatesVideo.chalice b/Chalice/refinements/DuplicatesVideo.chalice index abb2a429..175f0e8c 100644 --- a/Chalice/refinements/DuplicatesVideo.chalice +++ b/Chalice/refinements/DuplicatesVideo.chalice @@ -2,7 +2,7 @@ class Duplicates0 { method find(s:seq<int>) returns (b: bool)
requires forall i in s :: i in [0..100];
{
- spec b [b <==> exists i in [0..|s|] :: s[i] in s[..i] ];
+ b := exists i in [0..|s|] :: s[i] in s[..i];
}
}
@@ -22,7 +22,7 @@ class Duplicates1 refines Duplicates0 { }
}
-class Dupllcates2 refines Duplicates1 {
+class Duplicates2 refines Duplicates1 {
transforms find(s: seq<int>) returns (b: bool)
{
_;
@@ -36,7 +36,7 @@ class Dupllcates2 refines Duplicates1 { var c: bool := bitset[ s[n] ];
}
bitset := bitset[..s[n] ] ++ [true] ++ bitset[ s[n] + 1 ..];
- _
+ _;
}
}
}
\ No newline at end of file |