Chalice: Added axioms about div and mod. Updated DuplicatesVideo.chalice

2 files changed, 20 insertions, 4 deletions

diff --git a/Chalice/refinements/DuplicatesVideo.chalice b/Chalice/refinements/DuplicatesVideo.chalice
index 175f0e8c..f70fb82f 100644
--- a/Chalice/refinements/DuplicatesVideo.chalice
+++ b/Chalice/refinements/DuplicatesVideo.chalice
@@ -1,5 +1,5 @@
 class Duplicates0 {

-  method find(s:seq<int>) returns (b: bool)

+  method Find(s: seq<int>) returns (b: bool)

     requires forall i in s :: i in [0..100];

   {

     b := exists i in [0..|s|] :: s[i] in s[..i];

@@ -7,7 +7,7 @@ class Duplicates0 {
 }

 

 class Duplicates1 refines Duplicates0 {

-  refines find(s:seq<int>) returns (b: bool)

+  refines Find(s: seq<int>) returns (b: bool)

   {

     var n := 0;

     b := false;

@@ -15,7 +15,7 @@ class Duplicates1 refines Duplicates0 {
       invariant 0 <= n && n <= |s|;

       invariant b <==> exists i in [0..n] :: s[i] in s[..i];

     {

-      spec c:bool [c <==> s[n] in s[..n] ];

+	  var c := s[n] in s[..n];

       b := b || c;

       n := n + 1;

     }

@@ -23,9 +23,10 @@ class Duplicates1 refines Duplicates0 {
 }

 

 class Duplicates2 refines Duplicates1 {

-  transforms find(s: seq<int>) returns (b: bool)

+  transforms Find(s: seq<int>) returns (b: bool)

   {

     _;

+	// bitset has length 100, initially all false

     var bitset:seq<bool> [|bitset| == 100 && true !in bitset ];

     while

       invariant |bitset| == 100;

diff --git a/Chalice/src/Prelude.scala b/Chalice/src/Prelude.scala
index 1d127c76..a9e00ace 100644
--- a/Chalice/src/Prelude.scala
+++ b/Chalice/src/Prelude.scala
@@ -280,6 +280,21 @@ axiom (forall m1: MaskType, m2: MaskType :: {submask(m1, m2)}
 );

 

 // ---------------------------------------------------------------

+// -- Arithmetic -------------------------------------------------

+// ---------------------------------------------------------------

+

+// the connection between % and /

+axiom (forall x:int, y:int :: {x % y} {x / y}  x % y == x - x / y * y);

+

+// sign of denominator determines sign of remainder

+axiom (forall x:int, y:int :: {x % y}  0 < y  ==>  0 <= x % y  &&  x % y < y);

+axiom (forall x:int, y:int :: {x % y}  y < 0  ==>  y < x % y  &&  x % y <= 0);

+

+// the following axiom has some unfortunate matching, but it does state a property about % that

+// is sometime useful

+axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b  ==>  a + d <= b);

+

+// ---------------------------------------------------------------

 // -- End of prelude ---------------------------------------------

 // ---------------------------------------------------------------

 """