summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Binaries/DafnyPrelude.bpl28
-rw-r--r--Source/Dafny/Translator.cs22
-rw-r--r--Test/dafny0/Answer4
-rw-r--r--Test/dafny0/Basics.dfy75
-rw-r--r--Test/dafny0/MultiSets.dfy72
-rw-r--r--Test/vstte2012/runtest.bat2
6 files changed, 188 insertions, 15 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index a89ded50..dd0a6671 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -25,7 +25,9 @@ axiom (forall<T> s: Set T :: { Set#Card(s) } 0 <= Set#Card(s));
function Set#Empty<T>(): Set T;
axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);
-axiom (forall<T> s: Set T :: { Set#Card(s) } Set#Card(s) == 0 <==> s == Set#Empty());
+axiom (forall<T> s: Set T :: { Set#Card(s) }
+ (Set#Card(s) == 0 <==> s == Set#Empty()) &&
+ (Set#Card(s) != 0 ==> (exists x: T :: s[x])));
function Set#Singleton<T>(T): Set T;
axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);
@@ -117,8 +119,8 @@ type MultiSet T = [T]int;
function $IsGoodMultiSet<T>(ms: MultiSet T): bool;
// ints are non-negative, used after havocing, and for conversion from sequences to multisets.
axiom (forall<T> ms: MultiSet T :: { $IsGoodMultiSet(ms) }
- $IsGoodMultiSet(ms) <==> (forall o: T :: { ms[o] } 0 <= ms[o]));
-
+ $IsGoodMultiSet(ms) <==> (forall bx: T :: { ms[bx] } 0 <= ms[bx]));
+
function MultiSet#Card<T>(MultiSet T): int;
axiom (forall<T> s: MultiSet T :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s));
axiom (forall<T> s: MultiSet T, x: T, n: int :: { MultiSet#Card(s[x := n]) }
@@ -126,7 +128,9 @@ axiom (forall<T> s: MultiSet T, x: T, n: int :: { MultiSet#Card(s[x := n]) }
function MultiSet#Empty<T>(): MultiSet T;
axiom (forall<T> o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0);
-axiom (forall<T> s: MultiSet T :: { MultiSet#Card(s) } MultiSet#Card(s) == 0 <==> s == MultiSet#Empty());
+axiom (forall<T> s: MultiSet T :: { MultiSet#Card(s) }
+ (MultiSet#Card(s) == 0 <==> s == MultiSet#Empty()) &&
+ (MultiSet#Card(s) != 0 ==> (exists x: T :: 0 < s[x])));
function MultiSet#Singleton<T>(T): MultiSet T;
axiom (forall<T> r: T, o: T :: { MultiSet#Singleton(r)[o] } (MultiSet#Singleton(r)[o] == 1 <==> r == o) &&
@@ -470,14 +474,18 @@ function $IsCanonicalBoolBox(BoxType): bool;
axiom $IsCanonicalBoolBox($Box(false)) && $IsCanonicalBoolBox($Box(true));
axiom (forall b: BoxType :: { $Unbox(b): bool } $IsCanonicalBoolBox(b) ==> $Box($Unbox(b): bool) == b);
-// The following function and axiom are used to obtain a $Box($Unbox(_)) wrapper around
-// certain expressions. Note that it assumes any booleans contained in the set are canonical
-// (which is the case for any set that occurs in an execution of a Dafny program).
+// The following functions and axioms are used to obtain a $Box($Unbox(_)) wrapper around
+// certain expressions. Note that it assumes any booleans (or, indeed, values of any type) contained
+// in the (multi)set are canonical (which is the case for any (multi)set that occurs in an execution of
+// a Dafny program).
// The role of the parameter 'dummy' in the following is (an unfortunately clumsy construction
// whose only purpose is) simply to tell Boogie how to instantiate the type parameter 'T'.
-function $IsGoodSet<T>(s: Set BoxType, dummy: T): bool;
-axiom (forall<T> ss: Set BoxType, dummy: T, bx: BoxType :: { $IsGoodSet(ss, dummy), ss[bx] }
- $IsGoodSet(ss, dummy) ==> ss[bx] ==> bx == $Box($Unbox(bx):T));
+function $IsGoodSet_Extended<T>(s: Set BoxType, dummy: T): bool;
+axiom (forall<T> ss: Set BoxType, dummy: T, bx: BoxType :: { $IsGoodSet_Extended(ss, dummy), ss[bx] }
+ $IsGoodSet_Extended(ss, dummy) ==> ss[bx] ==> bx == $Box($Unbox(bx): T));
+function $IsGoodMultiSet_Extended<T>(ms: MultiSet BoxType, dummy: T): bool;
+axiom (forall<T> ms: MultiSet BoxType, dummy: T, bx: BoxType :: { $IsGoodMultiSet_Extended(ms, dummy), ms[bx] }
+ $IsGoodMultiSet_Extended(ms, dummy) ==> 0 < ms[bx] ==> bx == $Box($Unbox(bx): T));
// ---------------------------------------------------------------
// -- Encoding of type names -------------------------------------
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 9628f14b..242d6589 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -6504,10 +6504,18 @@ namespace Microsoft.Dafny {
type = type.Normalize();
if (type is SetType) {
var t = (SetType)type;
- // $IsGoodSet(x, V), where V is a value whose type is the same as the element type of the set.
+ // $IsGoodSet_Extended(x, V), where V is a value whose type is the same as the element type of the set.
var ex = ExemplaryBoxValue(t.Arg);
if (ex != null) {
- var p = FunctionCall(tok, "$IsGoodSet", Bpl.Type.Bool, x, ex);
+ var p = FunctionCall(tok, BuiltinFunction.IsGoodSet_Extended, null, x, ex);
+ r = r == null ? p : BplAnd(r, p);
+ }
+ } else if (type is MultiSetType) {
+ var t = (MultiSetType)type;
+ // $IsGoodMultiSet_Extended(x, V), where V is a value whose type is the same as the element type of the set.
+ var ex = ExemplaryBoxValue(t.Arg);
+ if (ex != null) {
+ var p = FunctionCall(tok, BuiltinFunction.IsGoodMultiSet_Extended, null, x, ex);
r = r == null ? p : BplAnd(r, p);
}
} else if (type.IsDatatype) {
@@ -8559,6 +8567,7 @@ namespace Microsoft.Dafny {
SetEqual,
SetSubset,
SetDisjoint,
+ IsGoodSet_Extended,
MultiSetCard,
MultiSetEmpty,
@@ -8572,6 +8581,7 @@ namespace Microsoft.Dafny {
MultiSetFromSet,
MultiSetFromSeq,
IsGoodMultiSet,
+ IsGoodMultiSet_Extended,
SeqLength,
SeqEmpty,
@@ -8671,6 +8681,10 @@ namespace Microsoft.Dafny {
Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Set#Disjoint", Bpl.Type.Bool, args);
+ case BuiltinFunction.IsGoodSet_Extended:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "$IsGoodSet_Extended", Bpl.Type.Bool, args);
case BuiltinFunction.MultiSetCard:
Contract.Assert(args.Length == 1);
@@ -8722,6 +8736,10 @@ namespace Microsoft.Dafny {
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "$IsGoodMultiSet", Bpl.Type.Bool, args);
+ case BuiltinFunction.IsGoodMultiSet_Extended:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "$IsGoodMultiSet_Extended", Bpl.Type.Bool, args);
case BuiltinFunction.SeqLength:
Contract.Assert(args.Length == 1);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 40725691..e78110b7 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -738,7 +738,7 @@ Basics.dfy(235,10): Error: when left-hand sides 0 and 1 refer to the same locati
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 37 verified, 11 errors
+Dafny program verifier finished with 51 verified, 11 errors
-------------------- ControlStructures.dfy --------------------
ControlStructures.dfy(5,3): Error: missing case in case statement: Purple
@@ -1475,7 +1475,7 @@ Execution trace:
(0,0): anon4_Then
(0,0): anon3
-Dafny program verifier finished with 39 verified, 3 errors
+Dafny program verifier finished with 53 verified, 3 errors
-------------------- PredExpr.dfy --------------------
PredExpr.dfy(4,12): Error: condition in assert expression might not hold
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index 6b1b366d..3d2e35bd 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -262,3 +262,78 @@ predicate MSFE(s: seq<int>)
copredicate CoPredTypeCheck(n: int)
requires n != 0;
+
+// -------------------- set cardinality ----------------------------------
+
+module SetCardinality {
+ method A(s: set<int>)
+ requires s != {};
+ {
+ if {
+ case true => assert s != {};
+ case true => assert |s| != 0;
+ case true => assert exists x :: x in s;
+ case true => var y :| y in s;
+ }
+ }
+
+ method B(s: set<int>)
+ requires |s| != 0;
+ {
+ if {
+ case true => assert s != {};
+ case true => assert |s| != 0;
+ case true => assert exists x :: x in s;
+ case true => var y :| y in s;
+ }
+ }
+
+ method C(s: set<int>)
+ requires exists x :: x in s;
+ {
+ if {
+ case true => assert s != {};
+ case true => assert |s| != 0;
+ case true => assert exists x :: x in s;
+ case true => var y :| y in s;
+ }
+ }
+
+ method A'(s: set<int>)
+ requires s == {};
+ {
+ if {
+ case true => assert s == {};
+ case true => assert |s| == 0;
+ case true => assert !exists x :: x in s;
+ case true => var y :| y !in s;
+ }
+ }
+
+ method B'(s: set<int>)
+ requires |s| == 0;
+ {
+ if {
+ case true => assert s == {};
+ case true => assert |s| == 0;
+ case true => assert !exists x :: x in s;
+ case true => var y :| y !in s;
+ }
+ }
+
+ method C'(s: set<int>)
+ requires forall x :: x !in s;
+ {
+ if {
+ case true => assert s == {};
+ case true => assert |s| == 0;
+ case true => assert !exists x :: x in s;
+ case true => var y :| y !in s;
+ }
+ }
+
+ method LetSuchThatExpression(s: set<int>)
+ ensures |s| != 0 ==> var x :| x in s; true;
+ {
+ }
+}
diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy
index a3a28222..ff03bb7a 100644
--- a/Test/dafny0/MultiSets.dfy
+++ b/Test/dafny0/MultiSets.dfy
@@ -176,3 +176,75 @@ method test12(a: nat, b: nat, c: int)
m2 := m2[true := c]; // error: c might be negative
}
+
+// ---------- cardinality ----------
+method MultisetCardinalityA(s: multiset<int>)
+ requires s != multiset{};
+{
+ if {
+ case true => assert s != multiset{};
+ case true => assert |s| != 0;
+ case true => assert exists x :: x in s;
+ case true => var y :| y in s;
+ }
+}
+
+method MultisetCardinalityB(s: multiset<int>)
+ requires |s| != 0;
+{
+ if {
+ case true => assert s != multiset{};
+ case true => assert |s| != 0;
+ case true => assert exists x :: x in s;
+ case true => var y :| y in s;
+ }
+}
+
+method MultisetCardinalityC(s: multiset<int>)
+ requires exists x :: x in s;
+{
+ if {
+ case true => assert s != multiset{};
+ case true => assert |s| != 0;
+ case true => assert exists x :: x in s;
+ case true => var y :| y in s;
+ }
+}
+
+method MultisetCardinalityA'(s: multiset<int>)
+ requires s == multiset{};
+{
+ if {
+ case true => assert s == multiset{};
+ case true => assert |s| == 0;
+ case true => assert !exists x :: x in s;
+ case true => var y :| y !in s;
+ }
+}
+
+method MultisetCardinalityB'(s: multiset<int>)
+ requires |s| == 0;
+{
+ if {
+ case true => assert s == multiset{};
+ case true => assert |s| == 0;
+ case true => assert !exists x :: x in s;
+ case true => var y :| y !in s;
+ }
+}
+
+method MultisetCardinalityC'(s: multiset<int>)
+ requires forall x :: x !in s;
+{
+ if {
+ case true => assert s == multiset{};
+ case true => assert |s| == 0;
+ case true => assert !exists x :: x in s;
+ case true => var y :| y !in s;
+ }
+}
+
+method LetSuchThatExpression(s: multiset<int>)
+ ensures |s| != 0 ==> var x :| x in s; true;
+{
+}
diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat
index 3fffb577..ecccd929 100644
--- a/Test/vstte2012/runtest.bat
+++ b/Test/vstte2012/runtest.bat
@@ -13,5 +13,5 @@ for %%f in (
) do (
echo.
echo -------------------- %%f --------------------
- %DAFNY_EXE% /compile:0 /vcsMaxKeepGoingSplits:2 /dprint:out.dfy.tmp %* %%f
+ %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 22:24:46 +0000