From 2fc9a47b200589fae14f698e7546553a0b31aec2 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Fri, 21 May 2010 18:38:47 +0000 Subject: Dafny: * Added arrays * Beefed up set axiomatization to know more things about set displays * Added a simple heuristic that can infer some simple decreases clauses for loops * Added Dafny solutions to a couple of VACID benchmarks --- Binaries/DafnyPrelude.bpl | 62 +++++++++++++++++++++++++++++++++++++++++++---- Binaries/DafnyRuntime.cs | 15 ++++++++++++ 2 files changed, 72 insertions(+), 5 deletions(-) (limited to 'Binaries') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index d9ff2f63..13314e29 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -2,7 +2,11 @@ // Created 9 February 2008 by Rustan Leino. // Converted to Boogie 2 on 28 June 2008. // Edited sequence axioms 20 October 2009 by Alex Summers. -// Copyright (c) 2008, Microsoft. +// Copyright (c) 2008-2010, Microsoft. + +// --------------------------------------------------------------- +// -- References ------------------------------------------------- +// --------------------------------------------------------------- type ref; const null: ref; @@ -23,6 +27,11 @@ axiom (forall r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> function Set#UnionOne(Set T, T) returns (Set T); axiom (forall a: Set T, x: T, o: T :: { Set#UnionOne(a,x)[o] } Set#UnionOne(a,x)[o] <==> o == x || a[o]); +axiom (forall a: Set T, x: T :: { Set#UnionOne(a, x) } + Set#UnionOne(a, x)[x]); +axiom (forall a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] } + a[y] ==> Set#UnionOne(a, x)[y]); + function Set#Union(Set T, Set T) returns (Set T); axiom (forall a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] } @@ -177,6 +186,8 @@ axiom (forall b: BoxType :: { $Unbox(b): Seq BoxType } $Box($Unbox(b): Seq BoxTy axiom (forall b: BoxType :: { $Unbox(b): DatatypeType } $Box($Unbox(b): DatatypeType) == b); // note: an axiom like this for bool would not be sound +// --------------------------------------------------------------- +// -- Encoding of type names ------------------------------------- // --------------------------------------------------------------- type ClassName; @@ -185,6 +196,7 @@ const unique class.bool: ClassName; const unique class.object: ClassName; const unique class.set: ClassName; const unique class.seq: ClassName; +const unique class.array: ClassName; function dtype(ref) returns (ClassName); function TypeParams(ref, int) returns (ClassName); @@ -198,6 +210,8 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) } TypeTupleCdr(TypeTuple(a,b)) == b); // --------------------------------------------------------------- +// -- Datatypes -------------------------------------------------- +// --------------------------------------------------------------- type DatatypeType; @@ -206,6 +220,8 @@ function DatatypeCtorId(DatatypeType) returns (DtCtorId); function DtRank(DatatypeType) returns (int); +// --------------------------------------------------------------- +// -- Axiom contexts --------------------------------------------- // --------------------------------------------------------------- // used to make sure function axioms are not used while their consistency is being checked @@ -213,19 +229,51 @@ const $ModuleContextHeight: int; const $FunctionContextHeight: int; const $InMethodContext: bool; +// --------------------------------------------------------------- +// -- Fields ----------------------------------------------------- // --------------------------------------------------------------- type Field alpha; -type HeapType = [ref,Field alpha]alpha; -function $IsGoodHeap(HeapType) returns (bool); -var $Heap: HeapType where $IsGoodHeap($Heap) && #cev_var_update(#cev_pc, cev_implicit, #loc.$Heap, $Heap); -const unique #loc.$Heap: $token; +type FieldCategory; +const unique $NamedField: FieldCategory; +const unique $IndexedField: FieldCategory; +function FCat(Field T): FieldCategory; const unique alloc: Field bool; +axiom FCat(alloc) == $NamedField; + +function IndexField(int): Field BoxType; +axiom (forall i: int :: { IndexField(i) } FCat(IndexField(i)) == $IndexedField); +function IndexField_Inverse(Field T): int; +axiom (forall i: int :: { IndexField(i) } IndexField_Inverse(IndexField(i)) == i); function DeclType(Field T) returns (ClassName); +// --------------------------------------------------------------- +// -- Arrays ----------------------------------------------------- +// --------------------------------------------------------------- + +function Array#Length(ref): int; +axiom (forall r: ref :: 0 <= Array#Length(r)); + +procedure UpdateArrayRange(arr: ref, low: int, high: int, rhs: BoxType); + modifies $Heap; + ensures $HeapSucc(old($Heap), $Heap); + ensures (forall i: int :: { $Heap[arr, IndexField(i)] } low <= i && i < high ==> $Heap[arr, IndexField(i)] == rhs); + ensures (forall o: ref, f: Field alpha :: { $Heap[o,f] } $Heap[o,f] == old($Heap)[o,f] || + (o == arr && FCat(f) == $IndexedField && low <= IndexField_Inverse(f) && IndexField_Inverse(f) < high)); + +// --------------------------------------------------------------- +// -- The heap --------------------------------------------------- +// --------------------------------------------------------------- + +type HeapType = [ref,Field alpha]alpha; + +function $IsGoodHeap(HeapType) returns (bool); +var $Heap: HeapType where $IsGoodHeap($Heap) && #cev_var_update(#cev_pc, cev_implicit, #loc.$Heap, $Heap); +const unique #loc.$Heap: $token; + function $HeapSucc(HeapType, HeapType) returns (bool); axiom (forall h: HeapType, r: ref, f: Field alpha, x: alpha :: { h[r,f:=x] } $HeapSucc(h, h[r,f:=x])); @@ -235,6 +283,8 @@ axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) } $HeapSucc(h,k) ==> (forall o: ref :: { k[o,alloc] } h[o,alloc] ==> k[o,alloc])); // --------------------------------------------------------------- +// -- Arithmetic ------------------------------------------------- +// --------------------------------------------------------------- // the connection between % and / axiom (forall x:int, y:int :: {x % y} {x / y} x % y == x - x / y * y); @@ -247,6 +297,8 @@ axiom (forall x:int, y:int :: {x % y} y < 0 ==> y < x % y && x % y <= 0); // 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); +// --------------------------------------------------------------- +// -- CEV (counterexample visualizer) ---------------------------- // --------------------------------------------------------------- type $token; diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 982683b9..610cd2f3 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -218,4 +218,19 @@ namespace Dafny this.Cdr = b; } } + public class Helpers + { + public static T[] InitNewArray(BigInteger size) { + int sz = (int)size; + T[] a = new T[sz]; + BigInteger[] b = a as BigInteger[]; + if (b != null) { + BigInteger z = new BigInteger(0); + for (int i = 0; i < sz; i++) { + b[i] = z; + } + } + return a; + } + } } -- cgit v1.2.3