Chalice:

* add sequence axiom updates from Dafny
* fix a bug in pretty printer for functions and predicates
* add a command line option for not checking termination; refactor options code to update syntax help string
* relax resolver to allow ghost state in assume statements (we don't know how to compile them in general anyways; assume false is still a special case and is compiled into assert false)

1 files changed, 19 insertions, 2 deletions

diff --git a/Chalice/src/Prelude.scala b/Chalice/src/Prelude.scala
index 2fb58697..b4994889 100644
--- a/Chalice/src/Prelude.scala
+++ b/Chalice/src/Prelude.scala
@@ -101,10 +101,18 @@ function IsGoodInhaleState(ih: HeapType, h: HeapType,
   (forall o: ref :: { h[o, rdheld] }  h[o, rdheld] ==> ih[o, mu] == h[o, mu])

 }

 

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

+// -- If then else -----------------------------------------------

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

+

 function ite<T>(bool, T, T) returns (T);

 axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} con ==> ite(con, a, b) == a);

 axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} ! con ==> ite(con, a, b) == b);

 

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

+// -- Axiomatization of sequences --------------------------------

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

+

 type Seq T;

 

 function Seq#Length<T>(Seq T) returns (int);

@@ -182,7 +190,7 @@ axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) }
   0 <= n ==>

     (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&

     (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s)));

-axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) }

+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) } {:weight 25}

   0 <= j && j < n && j < Seq#Length(s) ==>

     Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));

 

@@ -191,15 +199,24 @@ axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) }
   0 <= n ==>

     (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&

     (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0));

-axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) }

+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) } {:weight 25}

   0 <= n && 0 <= j && j < Seq#Length(s)-n ==>

     Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n));

 

+axiom (forall<T> s, t: Seq T ::

+  { Seq#Append(s, t) }

+  Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s &&

+  Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t);

+

 function Seq#Range(min: int, max: int) returns (Seq int);

 

 axiom (forall min: int, max: int :: { Seq#Length(Seq#Range(min, max)) } (min < max ==> Seq#Length(Seq#Range(min, max)) == max-min) && (max <= min ==> Seq#Length(Seq#Range(min, max)) == 0));

 axiom (forall min: int, max: int, j: int :: { Seq#Index(Seq#Range(min, max), j) } 0<=j && j<max-min ==> Seq#Index(Seq#Range(min, max), j) == min + j);

 

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

+// -- Permissions ------------------------------------------------

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

+

 axiom (forall h: HeapType, m: MaskType, o: ref, q: ref :: {wf(h, m), h[o, mu], h[q, mu]} wf(h, m) && o!=q && (0 < h[o, held] || h[o, rdheld]) && (0 < h[q, held] || h[q, rdheld]) ==> h[o, mu] != h[q, mu]);

 

 function DecPerm<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);