diff options
Diffstat (limited to 'Chalice/refinements/DuplicatesVideo.chalice')
| -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 |