Skip to content

Commit d2bdb19

Browse files
leoukleouk
committed
fixed some bag FAILED pos, and added concrete example with strings
1 parent 9991199 commit d2bdb19

2 files changed

Lines changed: 161 additions & 10 deletions

File tree

‎vdmlib/src/main/resources/Bag.vdmsl‎

Lines changed: 34 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -70,11 +70,15 @@ functions
7070
--@QuickCheck @T = nat;
7171
subbageq[@T]: Bag * Bag -> bool
7272
subbageq(a, b) ==
73-
forall xa in set dom a & amount[@T](a, a(xa)) <= amount[@T](b, b(xa))
73+
forall xa in set dom a & inbag[@T](xa, b) and amount[@T](a, xa) <= amount[@T](b, xa)
7474
pre
7575
type_convergent[@T](a) and type_convergent[@T](b)
7676
post
77-
bset[@T](a) subset bset[@T](b);
77+
RESULT <=>
78+
(bset[@T](a) subset bset[@T](b)
79+
and
80+
forall x in set bset[@T](a) & amount[@T](a, x) <= amount[@T](b, x)
81+
);
7882

7983
--@doc ZEves scale definition is wrong! wrt to theorem bagscaleBy1 (!
8084
--@QuickCheck @T = nat;
@@ -87,28 +91,48 @@ functions
8791
pre
8892
type_convergent[@T](b)
8993
post
90-
bset[@T](b) = bset[@T](RESULT)
91-
and
92-
type_convergent[@T](RESULT);
94+
type_convergent[@T](RESULT)
95+
and
96+
(bset[@T](RESULT) = if n = 0 then {} else bset[@T](b))
97+
and
98+
(forall x in set bset[@T](b) & amount[@T](RESULT, x) = n * amount[@T](b, x));
9399

94100
--@QuickCheck @T = nat;
95101
bunion[@T]: Bag * Bag -> Bag
96102
bunion(a, b) ==
97-
{ x |-> a(x) + b(x) | x in set dom a union dom b }
103+
--@doc unique of a + unique of b + common with summed amounts
104+
(bset[@T](b) <-: a)
105+
munion
106+
(bset[@T](a) <-: b)
107+
munion
108+
{ x |-> a(x) + b(x) | x in set dom a inter dom b }
98109
pre
99110
type_convergent[@T](a) and type_convergent[@T](b)
100111
post
101-
bset[@T](RESULT) = bset[@T](a) union bset[@T](b);
112+
bset[@T](RESULT) = bset[@T](a) union bset[@T](b)
113+
and
114+
(forall x in set bset[@T](a) inter bset[@T](b) & amount[@T](RESULT, x) = amount[@T](a, x) + amount[@T](b, x))
115+
and
116+
(forall x in set bset[@T](a) \ bset[@T](b) & amount[@T](RESULT, x) = amount[@T](a, x))
117+
and
118+
(forall x in set bset[@T](b) \ bset[@T](a) & amount[@T](RESULT, x) = amount[@T](b, x));
102119

103120
--@QuickCheck @T = nat;
104121
difference[@T]: Bag * Bag -> Bag
105122
difference(a, b) ==
106-
{ x |-> a(x) - b(x) | x in set dom a union dom b /*inter dom b*/ & a(x) - b(x) > 0 }
123+
--@doc unique of a with subtraction over common with b (or removal)
124+
bset[@T](b) <-: a
125+
munion
126+
{ x |-> a(x) - b(x) | x in set bset[@T](a) inter bset[@T](b) & a(x) > b(x) }
107127
pre
108128
type_convergent[@T](a) and type_convergent[@T](b)
109129
post
110-
--@doc not equal because when zeroed it goes out of the domain
111-
bset[@T](RESULT) subset bset[@T](a) \ bset[@T](b);
130+
--@doc resulting bag has elements of a with elements of b subtracted (or removed)
131+
(forall x in set bset[@T](RESULT) &
132+
amount[@T](RESULT, x) = max(0, amount[@T](a, x) - amount[@T](b, x)));
133+
134+
max: int * int -> int
135+
max(a, b) == if a >= b then a else b;
112136

113137
--@QuickCheck @T = nat;
114138
filter[@T]: seq of @T * (@T -> bool) -> seq of @T

‎vdmlib/src/main/resources/StrBag.vdmsl‎

Lines changed: 127 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,127 @@
1+
------------------------------------------------------------------------------------
2+
--@header
3+
--@doc Copyright Leo Freitas 2019-2023
4+
--@doc Bag as an abstract data type (inspired by SPARK ADTs and Z/Eves bags)
5+
------------------------------------------------------------------------------------
6+
module StrBag
7+
exports
8+
types
9+
Bag;
10+
struct String;
11+
functions
12+
empty: () -> Bag;
13+
isEmpty: Bag -> bool;
14+
bset: Bag -> set of String;
15+
inbag: String * Bag -> bool;
16+
count: Bag -> (String -> nat);
17+
amount: Bag * String -> nat;
18+
post_amount: Bag * String * nat +> bool;
19+
subbageq: Bag * Bag -> bool;
20+
scale: nat * Bag -> Bag;
21+
bunion: Bag * Bag -> Bag;
22+
post_bunion: Bag * Bag * Bag +> bool;
23+
difference: Bag * Bag -> Bag;
24+
post_difference: Bag * Bag * Bag +> bool;
25+
items: seq of String -> Bag;
26+
definitions
27+
types
28+
String = seq1 of char;
29+
Bag = map String to nat1;
30+
31+
functions
32+
empty: () -> Bag
33+
empty() == {|->};
34+
35+
isEmpty: Bag -> bool
36+
isEmpty(b) == b = empty()
37+
post
38+
RESULT <=> b = empty();
39+
40+
bset: Bag -> set of String
41+
bset(b) == dom b;
42+
43+
inbag: String * Bag -> bool
44+
inbag(x, b) == x in set bset(b)
45+
post
46+
RESULT <=> x in set bset(b);
47+
48+
count: Bag -> (String -> nat)
49+
count(b) == (lambda x: String & amount(b, x));
50+
51+
amount: Bag * String -> nat
52+
amount(b, x) ==
53+
if inbag(x, b) then b(x) else 0
54+
post
55+
(inbag(x, b) <=> is_nat1(RESULT));
56+
57+
--@QuickCheck String = nat;
58+
subbageq: Bag * Bag -> bool
59+
subbageq(a, b) ==
60+
forall xa in set dom a & inbag(xa, b) and amount(a, xa) <= amount(b, xa)
61+
post
62+
RESULT <=>
63+
(bset(a) subset bset(b)
64+
and
65+
forall x in set bset(a) & amount(a, x) <= amount(b, x)
66+
);
67+
68+
--@doc ZEves scale definition is wrong! wrt to theorem bagscaleBy1 (!
69+
--@QuickCheck String = nat;
70+
scale: nat * Bag -> Bag
71+
scale(n, b) ==
72+
if n = 0 then
73+
empty()
74+
else
75+
{ x |-> n * b(x) | x in set dom b }
76+
post
77+
bset(RESULT) = (if n = 0 then {} else bset(b))
78+
and
79+
(forall x in set bset(b) & amount(RESULT, x) = n * amount(b, x));
80+
81+
--@QuickCheck String = nat;
82+
bunion: Bag * Bag -> Bag
83+
bunion(a, b) ==
84+
--@doc unique of a + unique of b + common with summed amounts
85+
(bset(b) <-: a)
86+
munion
87+
(bset(a) <-: b)
88+
munion
89+
{ x |-> a(x) + b(x) | x in set dom a inter dom b }
90+
post
91+
bset(RESULT) = bset(a) union bset(b)
92+
and
93+
(forall x in set bset(a) inter bset(b) & amount(RESULT, x) = amount(a, x) + amount(b, x))
94+
and
95+
(forall x in set bset(a) \ bset(b) & amount(RESULT, x) = amount(a, x))
96+
and
97+
(forall x in set bset(b) \ bset(a) & amount(RESULT, x) = amount(b, x));
98+
99+
--@QuickCheck String = nat;
100+
difference: Bag * Bag -> Bag
101+
difference(a, b) ==
102+
--@doc unique of a with subtraction over common with b (or removal)
103+
bset(b) <-: a
104+
munion
105+
{ x |-> a(x) - b(x) | x in set bset(a) inter bset(b) & a(x) > b(x) }
106+
post
107+
--@doc resulting bag has elements of a with elements of b subtracted (or removed)
108+
(forall x in set bset(RESULT) &
109+
amount(RESULT, x) = max(0, amount(a, x) - amount(b, x)));
110+
111+
max: int * int -> int
112+
max(a, b) == if a >= b then a else b;
113+
114+
--@QuickCheck String = nat;
115+
filter: seq of String * (String -> bool) -> seq of String
116+
filter(s, f) == [ s(i) | i in set inds s & f(s(i)) ]
117+
post
118+
RESULT <> [] <=> (forall x in set elems RESULT & f(x));
119+
-- RESULT <> [] <=> elems RESULT = {x};
120+
121+
--@QuickCheck String = nat;
122+
items: seq of String -> Bag
123+
items(s) == { s(i) |-> len filter(s, (lambda x: String & s(i) = x)) | i in set inds s }
124+
post
125+
elems s = bset(RESULT);
126+
127+
end StrBag

0 commit comments

Comments
 (0)