diff options
author | 2011-11-09 10:31:35 -0800 | |
---|---|---|
committer | 2011-11-09 10:31:35 -0800 | |
commit | c38ad7de79e9a3b351ba9f1a8648f43893ec7ca7 (patch) | |
tree | 79513f9b3dbc86e42f607e3977b0341e2ecf5dbe | |
parent | 0c23ed8163bf437629cb4ef1649bcdf112eba93d (diff) |
Dafny: moved definition of class.array into prelude, anticipating writing axioms that use it
-rw-r--r-- | Binaries/DafnyPrelude.bpl | 9 | ||||
-rw-r--r-- | Source/Dafny/Translator.cs | 26 |
2 files changed, 29 insertions, 6 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 1fe21204..c954c019 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -326,6 +326,14 @@ axiom (forall<alpha> h: HeapType, o: ref, f: Field alpha, v: alpha, a: ref :: axiom (forall h: HeapType, i: int, v: BoxType, a: ref ::
{ Seq#FromArray(update(h, a, IndexField(i), v), a) }
0 <= i && i < array.Length(a) ==> Seq#FromArray(update(h, a, IndexField(i), v), a) == Seq#Update(Seq#FromArray(h, a), i, v) );
+/**** Someday:
+axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h, a) }
+ $IsGoodHeap(h) &&
+ a != null && read(h, a, alloc) && dtype(a) == class.array && TypeParams(a, 0) == class.bool
+ ==>
+ (forall i: int :: { Seq#Index(Seq#FromArray(h, a), i) }
+ 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> $IsCanonicalBoolBox(Seq#Index(Seq#FromArray(h, a), i))));
+****/
// Commutability of Take and Drop with Update.
axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
@@ -379,6 +387,7 @@ const unique class.bool: ClassName; const unique class.set: ClassName;
const unique class.seq: ClassName;
const unique class.multiset: ClassName;
+const unique class.array: ClassName;
function /*{:never_pattern true}*/ dtype(ref): ClassName;
function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName;
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 66cfbc57..e455561a 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -54,6 +54,7 @@ namespace Microsoft.Dafny { public readonly Bpl.Type DtCtorId;
public readonly Bpl.Expr Null;
private readonly Bpl.Constant allocField;
+ public readonly Bpl.Constant ClassDotArray;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(RefType != null);
@@ -71,6 +72,7 @@ namespace Microsoft.Dafny { Contract.Invariant(DtCtorId != null);
Contract.Invariant(Null != null);
Contract.Invariant(allocField != null);
+ Contract.Invariant(ClassDotArray != null);
}
@@ -116,7 +118,7 @@ namespace Microsoft.Dafny { Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.Function arrayLength, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,
Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType,
Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl dtCtorId,
- Bpl.Constant allocField) {
+ Bpl.Constant allocField, Bpl.Constant classDotArray) {
#region Non-null preconditions on parameters
Contract.Requires(refType != null);
Contract.Requires(boxType != null);
@@ -130,6 +132,7 @@ namespace Microsoft.Dafny { Contract.Requires(datatypeType != null);
Contract.Requires(dtCtorId != null);
Contract.Requires(allocField != null);
+ Contract.Requires(classDotArray != null);
#endregion
Bpl.CtorType refT = new Bpl.CtorType(Token.NoToken, refType, new Bpl.TypeSeq());
@@ -148,6 +151,7 @@ namespace Microsoft.Dafny { this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new Bpl.TypeSeq());
this.allocField = allocField;
this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);
+ this.ClassDotArray = classDotArray;
}
}
@@ -171,6 +175,7 @@ namespace Microsoft.Dafny { Bpl.TypeCtorDecl tickType = null;
Bpl.GlobalVariable heap = null;
Bpl.Constant allocField = null;
+ Bpl.Constant classDotArray = null;
foreach (var d in prog.TopLevelDeclarations) {
if (d is Bpl.TypeCtorDecl) {
Bpl.TypeCtorDecl dt = (Bpl.TypeCtorDecl)d;
@@ -203,6 +208,8 @@ namespace Microsoft.Dafny { Bpl.Constant c = (Bpl.Constant)d;
if (c.Name == "alloc") {
allocField = c;
+ } else if (c.Name == "class.array") {
+ classDotArray = c;
}
} else if (d is Bpl.GlobalVariable) {
Bpl.GlobalVariable v = (Bpl.GlobalVariable)d;
@@ -241,10 +248,12 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of $Heap");
} else if (allocField == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc");
+ } else if (classDotArray == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of class.array");
} else {
return new PredefinedDecls(refType, boxType, tickType,
setTypeCtor, multiSetTypeCtor, arrayLength, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,
- allocField);
+ allocField, classDotArray);
}
return null;
}
@@ -520,7 +529,11 @@ namespace Microsoft.Dafny { {
Contract.Requires(sink != null && predef != null);
Contract.Requires(c != null);
- sink.TopLevelDeclarations.Add(GetClass(c));
+ if (c.Name == "array") {
+ classes.Add(c, predef.ClassDotArray);
+ } else {
+ sink.TopLevelDeclarations.Add(GetClass(c));
+ }
foreach (MemberDecl member in c.Members) {
if (member is Field) {
@@ -4532,13 +4545,14 @@ namespace Microsoft.Dafny { Bpl.Expr xSubT = Bpl.Expr.Gt(Bpl.Expr.SelectTok(tok, x, t), Bpl.Expr.Literal(0));
Bpl.Expr unboxT = ExpressionTranslator.ModeledAsBoxType(st.Arg) ? t : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), t);
+ Bpl.Expr isGoodMultiset = FunctionCall(tok, BuiltinFunction.IsGoodMultiSet, null, x);
Bpl.Expr wh = GetWhereClause(tok, unboxT, st.Arg, etran);
if (wh != null) {
Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubT));
- return Bpl.Expr.And(FunctionCall(tok, BuiltinFunction.IsGoodMultiSet, Bpl.Type.Bool, x),
- new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh)));
+ var q = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh));
+ isGoodMultiset = Bpl.Expr.And(isGoodMultiset, q);
}
- return FunctionCall(tok, BuiltinFunction.IsGoodMultiSet, null, x);
+ return isGoodMultiset;
} else if (type is SeqType) {
SeqType st = (SeqType)type;
// (forall i: int :: { Seq#Index(x,i) }
|