From 10a8896ae40fd918abbb8caa616ac6ee0876ac1d Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 29 May 2015 16:29:15 -0700 Subject: Add an infinite set collection type. --- Binaries/DafnyPrelude.bpl | 91 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 91 insertions(+) (limited to 'Binaries') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 74bdb63e..5ee8b845 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -20,6 +20,7 @@ const unique TInt : Ty; const unique TNat : Ty; const unique TReal : Ty; function TSet(Ty) : Ty; +function TISet(Ty) : Ty; function TMultiSet(Ty) : Ty; function TSeq(Ty) : Ty; function TMap(Ty, Ty) : Ty; @@ -27,6 +28,8 @@ function TIMap(Ty, Ty) : Ty; function Inv0_TSet(Ty) : Ty; axiom (forall t: Ty :: { TSet(t) } Inv0_TSet(TSet(t)) == t); +function Inv0_TISet(Ty) : Ty; +axiom (forall t: Ty :: { TISet(t) } Inv0_TISet(TISet(t)) == t); function Inv0_TSeq(Ty) : Ty; axiom (forall t: Ty :: { TSeq(t) } Inv0_TSeq(TSeq(t)) == t); function Inv0_TMultiSet(Ty) : Ty; @@ -52,6 +55,7 @@ const unique TagInt : TyTag; const unique TagNat : TyTag; const unique TagReal : TyTag; const unique TagSet : TyTag; +const unique TagISet : TyTag; const unique TagMultiSet : TyTag; const unique TagSeq : TyTag; const unique TagMap : TyTag; @@ -64,6 +68,7 @@ axiom Tag(TInt) == TagInt; axiom Tag(TNat) == TagNat; axiom Tag(TReal) == TagReal; axiom (forall t: Ty :: { TSet(t) } Tag(TSet(t)) == TagSet); +axiom (forall t: Ty :: { TISet(t) } Tag(TISet(t)) == TagISet); axiom (forall t: Ty :: { TMultiSet(t) } Tag(TMultiSet(t)) == TagMultiSet); axiom (forall t: Ty :: { TSeq(t) } Tag(TSeq(t)) == TagSeq); axiom (forall t, u: Ty :: { TMap(t,u) } Tag(TMap(t,u)) == TagMap); @@ -137,6 +142,9 @@ axiom (forall bx : Box :: axiom (forall bx : Box, t : Ty :: { $IsBox(bx, TSet(t)) } ( $IsBox(bx, TSet(t)) ==> $Box($Unbox(bx) : Set Box) == bx && $Is($Unbox(bx) : Set Box, TSet(t)))); +axiom (forall bx : Box, t : Ty :: + { $IsBox(bx, TISet(t)) } + ( $IsBox(bx, TISet(t)) ==> $Box($Unbox(bx) : ISet Box) == bx && $Is($Unbox(bx) : ISet Box, TISet(t)))); axiom (forall bx : Box, t : Ty :: { $IsBox(bx, TMultiSet(t)) } ( $IsBox(bx, TMultiSet(t)) ==> $Box($Unbox(bx) : MultiSet Box) == bx && $Is($Unbox(bx) : MultiSet Box, TMultiSet(t)))); @@ -187,6 +195,10 @@ axiom (forall v: Set Box, t0: Ty :: { $Is(v, TSet(t0)) } $Is(v, TSet(t0)) <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsBox(bx, t0))); +axiom (forall v: ISet Box, t0: Ty :: { $Is(v, TISet(t0)) } + $Is(v, TISet(t0)) <==> + (forall bx: Box :: { v[bx] } + v[bx] ==> $IsBox(bx, t0))); axiom (forall v: MultiSet Box, t0: Ty :: { $Is(v, TMultiSet(t0)) } $Is(v, TMultiSet(t0)) <==> (forall bx: Box :: { v[bx] } @@ -202,6 +214,10 @@ axiom (forall v: Set Box, t0: Ty, h: Heap :: { $IsAlloc(v, TSet(t0), h) } $IsAlloc(v, TSet(t0), h) <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsAllocBox(bx, t0, h))); +axiom (forall v: ISet Box, t0: Ty, h: Heap :: { $IsAlloc(v, TISet(t0), h) } + $IsAlloc(v, TISet(t0), h) <==> + (forall bx: Box :: { v[bx] } + v[bx] ==> $IsAllocBox(bx, t0, h))); axiom (forall v: MultiSet Box, t0: Ty, h: Heap :: { $IsAlloc(v, TMultiSet(t0), h) } $IsAlloc(v, TMultiSet(t0), h) <==> (forall bx: Box :: { v[bx] } @@ -544,6 +560,81 @@ function Set#Disjoint(Set T, Set T): bool; axiom (forall a: Set T, b: Set T :: { Set#Disjoint(a,b) } Set#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o])); +// --------------------------------------------------------------- +// -- Axiomatization of isets ------------------------------------- +// --------------------------------------------------------------- + +type ISet T = [T]bool; + +function ISet#Empty(): Set T; +axiom (forall o: T :: { ISet#Empty()[o] } !ISet#Empty()[o]); + +// the empty set could be of anything +//axiom (forall t: Ty :: { $Is(ISet#Empty() : [T]bool, TISet(t)) } $Is(ISet#Empty() : [T]bool, TISet(t))); + + +function ISet#UnionOne(ISet T, T): ISet T; +axiom (forall a: ISet T, x: T, o: T :: { ISet#UnionOne(a,x)[o] } + ISet#UnionOne(a,x)[o] <==> o == x || a[o]); +axiom (forall a: ISet T, x: T :: { ISet#UnionOne(a, x) } + ISet#UnionOne(a, x)[x]); +axiom (forall a: ISet T, x: T, y: T :: { ISet#UnionOne(a, x), a[y] } + a[y] ==> ISet#UnionOne(a, x)[y]); + +function ISet#Union(ISet T, ISet T): ISet T; +axiom (forall a: ISet T, b: ISet T, o: T :: { ISet#Union(a,b)[o] } + ISet#Union(a,b)[o] <==> a[o] || b[o]); +axiom (forall a, b: ISet T, y: T :: { ISet#Union(a, b), a[y] } + a[y] ==> ISet#Union(a, b)[y]); +axiom (forall a, b: Set T, y: T :: { ISet#Union(a, b), b[y] } + b[y] ==> ISet#Union(a, b)[y]); +axiom (forall a, b: ISet T :: { ISet#Union(a, b) } + ISet#Disjoint(a, b) ==> + ISet#Difference(ISet#Union(a, b), a) == b && + ISet#Difference(ISet#Union(a, b), b) == a); +// Follows from the general union axiom, but might be still worth including, because disjoint union is a common case: +// axiom (forall a, b: ISet T :: { ISet#Card(ISet#Union(a, b)) } +// ISet#Disjoint(a, b) ==> +// ISet#Card(ISet#Union(a, b)) == ISet#Card(a) + ISet#Card(b)); + +function ISet#Intersection(ISet T, ISet T): ISet T; +axiom (forall a: ISet T, b: ISet T, o: T :: { ISet#Intersection(a,b)[o] } + ISet#Intersection(a,b)[o] <==> a[o] && b[o]); + +axiom (forall a, b: ISet T :: { ISet#Union(ISet#Union(a, b), b) } + ISet#Union(ISet#Union(a, b), b) == ISet#Union(a, b)); +axiom (forall a, b: Set T :: { ISet#Union(a, ISet#Union(a, b)) } + ISet#Union(a, ISet#Union(a, b)) == ISet#Union(a, b)); +axiom (forall a, b: ISet T :: { ISet#Intersection(ISet#Intersection(a, b), b) } + ISet#Intersection(ISet#Intersection(a, b), b) == ISet#Intersection(a, b)); +axiom (forall a, b: ISet T :: { ISet#Intersection(a, ISet#Intersection(a, b)) } + ISet#Intersection(a, ISet#Intersection(a, b)) == ISet#Intersection(a, b)); + + +function ISet#Difference(ISet T, ISet T): ISet T; +axiom (forall a: ISet T, b: ISet T, o: T :: { ISet#Difference(a,b)[o] } + ISet#Difference(a,b)[o] <==> a[o] && !b[o]); +axiom (forall a, b: ISet T, y: T :: { ISet#Difference(a, b), b[y] } + b[y] ==> !ISet#Difference(a, b)[y] ); + +function ISet#Subset(ISet T, ISet T): bool; +axiom(forall a: ISet T, b: ISet T :: { ISet#Subset(a,b) } + ISet#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] ==> b[o])); +// axiom(forall a: ISet T, b: ISet T :: +// { ISet#Subset(a,b), ISet#Card(a), ISet#Card(b) } // very restrictive trigger +// ISet#Subset(a,b) ==> ISet#Card(a) <= ISet#Card(b)); + + +function ISet#Equal(ISet T, ISet T): bool; +axiom(forall a: ISet T, b: ISet T :: { ISet#Equal(a,b) } + ISet#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <==> b[o])); +axiom(forall a: ISet T, b: ISet T :: { ISet#Equal(a,b) } // extensionality axiom for sets + ISet#Equal(a,b) ==> a == b); + +function ISet#Disjoint(ISet T, ISet T): bool; +axiom (forall a: ISet T, b: ISet T :: { ISet#Disjoint(a,b) } + ISet#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o])); + // --------------------------------------------------------------- // -- Axiomatization of multisets -------------------------------- // --------------------------------------------------------------- -- cgit v1.2.3