From 7fe04f35f93d5d1c5f8461b595c0c096476c843e Mon Sep 17 00:00:00 2001 From: yizhou7 Date: Sun, 10 Oct 2021 18:46:02 -0400 Subject: [PATCH 1/8] removed some tiggers that repeats dafny, added some comments for dafny selected trigger --- src/Collections/Maps/Imaps.dfy | 11 ++++++- src/Collections/Maps/Maps.dfy | 12 ++++++- src/Collections/Sequences/Seq.dfy | 54 +++++++++++++++++-------------- src/Collections/Sets/Isets.dfy | 9 ++++-- src/Collections/Sets/Sets.dfy | 23 +++++++------ 5 files changed, 71 insertions(+), 38 deletions(-) diff --git a/src/Collections/Maps/Imaps.dfy b/src/Collections/Maps/Imaps.dfy index 72720fa1..9a533bf0 100644 --- a/src/Collections/Maps/Imaps.dfy +++ b/src/Collections/Maps/Imaps.dfy @@ -22,7 +22,9 @@ module Imaps { /* Remove all key-value pairs corresponding to the iset of keys provided. */ function {:opaque} RemoveKeys(m: imap, xs: iset): (m': imap) + /* Dafny selected triggers: {m[x]}, {m'[x]}, {x in m'}, {x in xs}, {x in m} */ ensures forall x {:trigger m'[x]} :: x in m && x !in xs ==> x in m' && m'[x] == m[x] + /* Dafny selected triggers: {x in xs}, {x in m}, {x in m'} */ ensures forall x {:trigger x in m'} :: x in m' ==> x in m && x !in xs ensures m'.Keys == m.Keys - xs { @@ -32,6 +34,7 @@ module Imaps { /* Remove a key-value pair. Returns unmodified imap if key is not found. */ function {:opaque} RemoveKey(m: imap, x: X): (m': imap) ensures m' == RemoveKeys(m, iset{x}) + /* Dafny selected triggers: {m[x']}, {m'[x']}, {x' in m'} */ ensures forall x' {:trigger m'[x']} :: x' in m' ==> m'[x'] == m[x'] { imap i | i in m && i != x :: m[i] @@ -54,14 +57,16 @@ module Imaps { predicate IsSubset(m: imap, m': imap) { && m.Keys <= m'.Keys - && forall x {:trigger EqualOnKey(m, m', x)}{:trigger x in m} :: x in m ==> EqualOnKey(m, m', x) + && forall x :: x in m ==> EqualOnKey(m, m', x) } /* Union of two imaps. Does not require disjoint domains; on the intersection, values from the second imap are chosen. */ function {:opaque} Union(m: imap, m': imap): (r: imap) ensures r.Keys == m.Keys + m'.Keys + /* Dafny selected triggers: {m'[x]}, {r[x]}, {x in m'} */ ensures forall x {:trigger r[x]} :: x in m' ==> r[x] == m'[x] + /* Dafny selected triggers: {m[x]}, {r[x]}, {x in m'}, {x in m} */ ensures forall x {:trigger r[x]} :: x in m && x !in m' ==> r[x] == m[x] { m + m' @@ -70,6 +75,7 @@ module Imaps { /* True iff an imap is injective. */ predicate {:opaque} Injective(m: imap) { + /* Dafny selected triggers: {m[x'], m[x]}, {m[x'], x in m}, {m[x], x' in m}, {x' in m, x in m} */ forall x, x' {:trigger m[x], m[x']} :: x != x' && x in m && x' in m ==> m[x] != m[x'] } @@ -91,12 +97,14 @@ module Imaps { /* True iff an imap contains all valid keys. */ predicate {:opaque} Total(m: imap) { + /* Dafny selected triggers: {i in m} */ forall i {:trigger m[i]}{:trigger i in m} :: i in m } /* True iff an imap is monotonic. */ predicate {:opaque} Monotonic(m: imap) { + /* Dafny selected triggers: {m[x'], m[x]}, {m[x'], x in m}, {m[x], x' in m}, {x' in m, x in m} */ forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && x <= x' ==> m[x] <= m[x'] } @@ -104,6 +112,7 @@ module Imaps { equal to start. */ predicate {:opaque} MonotonicFrom(m: imap, start: int) { + /* Dafny selected triggers: {m[x'], m[x]}, {m[x'], x in m}, {m[x], x' in m}, {x' in m, x in m} */ forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && start <= x <= x' ==> m[x] <= m[x'] } diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy index b06e65cd..12f85fec 100644 --- a/src/Collections/Maps/Maps.dfy +++ b/src/Collections/Maps/Maps.dfy @@ -21,7 +21,9 @@ module Maps { } function method {:opaque} ToImap(m: map): (m': imap) + /* Dafny selected triggers: {m[x]}, {m'[x]}, {x in m'}, {x in m} */ ensures forall x {:trigger m'[x]} :: x in m ==> x in m' && m'[x] == m[x] + /* Dafny selected triggers: {x in m}, {x in m'} */ ensures forall x {:trigger x in m'} :: x in m' ==> x in m { imap x | x in m :: m[x] @@ -29,7 +31,9 @@ module Maps { /* Remove all key-value pairs corresponding to the set of keys provided. */ function method {:opaque} RemoveKeys(m: map, xs: set): (m': map) + /* Dafny selected triggers: {m[x]}, {m'[x]}, {x in m'}, {x in xs}, {x in m} */ ensures forall x {:trigger m'[x]} :: x in m && x !in xs ==> x in m' && m'[x] == m[x] + /* Dafny selected triggers: {x in xs}, {x in m}, {x in m'} */ ensures forall x {:trigger x in m'} :: x in m' ==> x in m && x !in xs ensures m'.Keys == m.Keys - xs { @@ -65,14 +69,16 @@ module Maps { predicate IsSubset(m: map, m': map) { && m.Keys <= m'.Keys - && forall x {:trigger EqualOnKey(m, m', x)}{:trigger x in m} :: x in m ==> EqualOnKey(m, m', x) + && forall x :: x in m ==> EqualOnKey(m, m', x) } /* Union of two maps. Does not require disjoint domains; on the intersection, values from the second map are chosen. */ function method {:opaque} Union(m: map, m': map): (r: map) ensures r.Keys == m.Keys + m'.Keys + /* Dafny selected triggers: {m'[x]}, {r[x]}, {x in m'} */ ensures forall x {:trigger r[x]} :: x in m' ==> r[x] == m'[x] + /* Dafny selected triggers: {m[x]}, {r[x]}, {x in m'}, {x in m} */ ensures forall x {:trigger r[x]} :: x in m && x !in m' ==> r[x] == m[x] { m + m' @@ -91,6 +97,7 @@ module Maps { /* True iff a map is injective. */ predicate {:opaque} Injective(m: map) { + /* Dafny selected triggers: {m[x'], m[x]}, {m[x'], x in m}, {m[x], x' in m}, {x' in m, x in m} */ forall x, x' {:trigger m[x], m[x']} :: x != x' && x in m && x' in m ==> m[x] != m[x'] } @@ -112,12 +119,14 @@ module Maps { /* True iff a map contains all valid keys. */ predicate {:opaque} Total(m: map) { + /* Dafny selected triggers: {i in m} */ forall i {:trigger m[i]}{:trigger i in m} :: i in m } /* True iff a map is monotonic. */ predicate {:opaque} Monotonic(m: map) { + /* Dafny selected triggers: {m[x'], m[x]}, {m[x'], x in m}, {m[x], x' in m}, {x' in m, x in m} */ forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && x <= x' ==> m[x] <= m[x'] } @@ -125,6 +134,7 @@ module Maps { equal to start. */ predicate {:opaque} MonotonicFrom(m: map, start: int) { + /* Dafny selected triggers: {m[x'], m[x]}, {m[x'], x in m}, {m[x], x' in m}, {x' in m, x in m} */ forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && start <= x <= x' ==> m[x] <= m[x'] } diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 2eb850c9..4e425b24 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -120,7 +120,7 @@ module Seq { var r2 := r1[s2..e2]; var r3 := s[s1+s2..s1+e2]; assert |r2| == |r3|; - forall i {:trigger r2[i], r3[i]}| 0 <= i < |r2| ensures r2[i] == r3[i]; + forall i | 0 <= i < |r2| ensures r2[i] == r3[i]; { } } @@ -166,7 +166,7 @@ module Seq { /* is true if there are no duplicate values in the sequence */ predicate {:opaque} HasNoDuplicates(s: seq) { - (forall i, j {:trigger s[i], s[j]}:: 0 <= i < |s| && 0 <= j < |s| && i != j ==> s[i] != s[j]) + (forall i, j :: 0 <= i < |s| && 0 <= j < |s| && i != j ==> s[i] != s[j]) } /* if sequence a and b don't have duplicates and there are no elements in @@ -181,7 +181,7 @@ module Seq { reveal HasNoDuplicates(); var c := a + b; if |c| > 1 { - assert forall i, j {:trigger c[i], c[j]}:: i != j && 0 <= i < |a| && |a| <= j < |c| ==> + assert forall i, j :: i != j && 0 <= i < |a| && |a| <= j < |c| ==> c[i] in multiset(a) && c[j] in multiset(b) && c[i] != c[j]; } } @@ -203,7 +203,7 @@ module Seq { /* proves that there are no duplicate values in the multiset version of the sequence */ lemma LemmaMultisetHasNoDuplicates(s: seq) requires HasNoDuplicates(s) - ensures forall x {:trigger multiset(s)[x]} | x in multiset(s):: multiset(s)[x] == 1 + ensures forall x | x in multiset(s):: multiset(s)[x] == 1 { if |s| == 0 { } else { @@ -222,7 +222,7 @@ module Seq { function method {:opaque} IndexOf(s: seq, v: T): (i: nat) requires v in s ensures i < |s| && s[i] == v - ensures forall j {:trigger s[j]} :: 0 <= j < i ==> s[j] != v + ensures forall j :: 0 <= j < i ==> s[j] != v { if s[0] == v then 0 else 1 + IndexOf(s[1..], v) } @@ -231,7 +231,7 @@ module Seq { found */ function method {:opaque} IndexOfOption(s: seq, v: T): (o: Option) ensures if o.Some? then o.value < |s| && s[o.value] == v && - forall j {:trigger s[j]} :: 0 <= j < o.value ==> s[j] != v + forall j :: 0 <= j < o.value ==> s[j] != v else v !in s { if |s| == 0 then None() @@ -246,7 +246,7 @@ module Seq { function method {:opaque} LastIndexOf(s: seq, v: T): (i: nat) requires v in s ensures i < |s| && s[i] == v - ensures forall j {:trigger s[j]} :: i < j < |s| ==> s[j] != v + ensures forall j :: i < j < |s| ==> s[j] != v { if s[|s|-1] == v then |s| - 1 else LastIndexOf(s[..|s|-1], v) } @@ -255,7 +255,7 @@ module Seq { found */ function method {:opaque} LastIndexOfOption(s: seq, v: T): (o: Option) ensures if o.Some? then o.value < |s| && s[o.value] == v && - forall j {:trigger s[j]} :: o.value < j < |s| ==> s[j] != v + forall j :: o.value < j < |s| ==> s[j] != v else v !in s { if |s| == 0 then None() @@ -266,8 +266,8 @@ module Seq { function method {:opaque} Remove(s: seq, pos: nat): (s': seq) requires pos < |s| ensures |s'| == |s| - 1 - ensures forall i {:trigger s'[i], s[i]} | 0 <= i < pos :: s'[i] == s[i] - ensures forall i {:trigger s'[i]} | pos <= i < |s| - 1 :: s'[i] == s[i+1] + ensures forall i | 0 <= i < pos :: s'[i] == s[i] + ensures forall i| pos <= i < |s| - 1 :: s'[i] == s[i+1] { s[..pos] + s[pos+1..] } @@ -292,8 +292,8 @@ module Seq { function method {:opaque} Insert(s: seq, a: T, pos: nat): seq requires pos <= |s| ensures |Insert(s, a, pos)| == |s| + 1 - ensures forall i {:trigger Insert(s, a, pos)[i], s[i]} :: 0 <= i < pos ==> Insert(s, a, pos)[i] == s[i] - ensures forall i {:trigger s[i]} :: pos <= i < |s| ==> Insert(s, a, pos)[i+1] == s[i] + ensures forall i :: 0 <= i < pos ==> Insert(s, a, pos)[i] == s[i] + ensures forall i :: pos <= i < |s| ==> Insert(s, a, pos)[i+1] == s[i] ensures Insert(s, a, pos)[pos] == a ensures multiset(Insert(s, a, pos)) == multiset(s) + multiset{a} { @@ -303,6 +303,7 @@ module Seq { function method {:opaque} Reverse(s: seq): (s': seq) ensures |s'| == |s| + /* Dafny selected triggers: {s'[i]} */ ensures forall i {:trigger s'[i]}{:trigger s[|s| - i - 1]} :: 0 <= i < |s| ==> s'[i] == s[|s| - i - 1] { if s == [] then [] else [s[|s|-1]] + Reverse(s[0 .. |s|-1]) @@ -310,7 +311,7 @@ module Seq { function method {:opaque} Repeat(v: T, length: nat): (s: seq) ensures |s| == length - ensures forall i: nat {:trigger s[i]} | i < |s| :: s[i] == v + ensures forall i: nat | i < |s| :: s[i] == v { if length == 0 then [] @@ -321,6 +322,7 @@ module Seq { /* unzips a sequence that contains ordered pairs into 2 seperate sequences */ function method {:opaque} Unzip(s: seq<(A, B)>): (seq, seq) ensures |Unzip(s).0| == |Unzip(s).1| == |s| + /* Dafny selected triggers: {s[i]}, {Unzip(s).1[i]}, {Unzip(s).0[i]} */ ensures forall i {:trigger Unzip(s).0[i]} {:trigger Unzip(s).1[i]} :: 0 <= i < |s| ==> (Unzip(s).0[i], Unzip(s).1[i]) == s[i] { @@ -335,6 +337,7 @@ module Seq { function method {:opaque} Zip(a: seq, b: seq): seq<(A, B)> requires |a| == |b| ensures |Zip(a, b)| == |a| + /* Dafny selected triggers: {b[i]}, {a[i]}, {Zip(a, b)[i]} */ ensures forall i {:trigger Zip(a, b)[i]}:: 0 <= i < |Zip(a, b)| ==> Zip(a, b)[i] == (a[i], b[i]) ensures Unzip(Zip(a, b)).0 == a ensures Unzip(Zip(a, b)).1 == b @@ -358,7 +361,7 @@ module Seq { /* finds the maximum integer value in the sequence */ function method {:opaque} Max(s: seq): int requires 0 < |s| - ensures forall k {:trigger k in s} :: k in s ==> Max(s) >= k + ensures forall k :: k in s ==> Max(s) >= k ensures Max(s) in s { assert s == [s[0]] + s[1..]; @@ -371,6 +374,7 @@ module Seq { requires 0 < |a| && 0 < |b| ensures Max(a+b) >= Max(a) ensures Max(a+b) >= Max(b) + /* Dafny selected trigger: {i in a + b} */ ensures forall i {:trigger i in [Max(a + b)]} :: i in a + b ==> Max(a + b) >= i { reveal Max(); @@ -384,7 +388,7 @@ module Seq { /* finds the minimum integer value in the sequence */ function method {:opaque} Min(s: seq): int requires 0 < |s| - ensures forall k {:trigger k in s} :: k in s ==> Min(s) <= k + ensures forall k :: k in s ==> Min(s) <= k ensures Min(s) in s { assert s == [s[0]] + s[1..]; @@ -397,7 +401,8 @@ module Seq { requires 0 < |a| && 0 < |b| ensures Min(a+b) <= Min(a) ensures Min(a+b) <= Min(b) - ensures forall i {:trigger i in a + b} :: i in a + b ==> Min(a + b) <= i + /* Dafny selected trigger: {i in a + b} */ + ensures forall i {:trigger i in a + b} :: i in a + b ==> Min(a + b) <= i { reveal Min(); if |a| == 1 { @@ -531,7 +536,7 @@ module Seq { than the length of the original sequence of sequences multiplied by the length of the longest sequence */ lemma LemmaFlattenLengthLeMul(s: seq>, j: int) - requires forall i {:trigger s[i]} | 0 <= i < |s| :: |s[i]| <= j + requires forall i | 0 <= i < |s| :: |s[i]| <= j ensures |FlattenReverse(s)| <= |s| * j { if |s| == 0 { @@ -549,10 +554,11 @@ module Seq { /* applies a transformation function on the sequence */ function method {:opaque} Map(f: (T ~> R), s: seq): (result: seq) - requires forall i {:trigger s[i]} :: 0 <= i < |s| ==> f.requires(s[i]) + requires forall i :: 0 <= i < |s| ==> f.requires(s[i]) ensures |result| == |s| + /* Dafny selected triggers: {s[i]}, {result[i]} */ ensures forall i {:trigger result[i]}:: 0 <= i < |s| ==> result[i] == f(s[i]); - reads set i, o {:trigger o in f.reads(s[i])} | 0 <= i < |s| && o in f.reads(s[i]):: o + reads set i, o | 0 <= i < |s| && o in f.reads(s[i]):: o { if |s| == 0 then [] else [f(s[0])] + Map(f, s[1..]) @@ -562,8 +568,8 @@ module Seq { Map on each sequence seperately and then concatenating the two resulting sequences */ lemma {:opaque} LemmaMapDistributesOverConcat(f: (T ~> R), a: seq, b: seq) - requires forall i {:trigger a[i]}:: 0 <= i < |a| ==> f.requires(a[i]) - requires forall j {:trigger b[j]}:: 0 <= j < |b| ==> f.requires(b[j]) + requires forall i :: 0 <= i < |a| ==> f.requires(a[i]) + requires forall j :: 0 <= j < |b| ==> f.requires(b[j]) ensures Map(f, a + b) == Map(f, a) + Map(f, b) { reveal Map(); @@ -585,7 +591,7 @@ module Seq { function method {:opaque} Filter(f: (T ~> bool), s: seq): (result: seq) requires forall i :: 0 <= i < |s| ==> f.requires(s[i]) ensures |result| <= |s| - ensures forall i: nat {:trigger result[i]} :: i < |result| && f.requires(result[i]) ==> f(result[i]) + ensures forall i: nat :: i < |result| && f.requires(result[i]) ==> f(result[i]) reads f.reads { if |s| == 0 then [] @@ -595,8 +601,8 @@ module Seq { /* concatenating two sequences and then using "filter" is the same as using "filter" on each sequences seperately and then concatenating their resulting sequences */ lemma {:opaque} LemmaFilterDistributesOverConcat(f: (T ~> bool), a: seq, b: seq) - requires forall i {:trigger a[i]}:: 0 <= i < |a| ==> f.requires(a[i]) - requires forall j {:trigger b[j]}:: 0 <= j < |b| ==> f.requires(b[j]) + requires forall i :: 0 <= i < |a| ==> f.requires(a[i]) + requires forall j :: 0 <= j < |b| ==> f.requires(b[j]) ensures Filter(f, a + b) == Filter(f, a) + Filter(f, b) { reveal Filter(); diff --git a/src/Collections/Sets/Isets.dfy b/src/Collections/Sets/Isets.dfy index c3a9fce4..64334646 100644 --- a/src/Collections/Sets/Isets.dfy +++ b/src/Collections/Sets/Isets.dfy @@ -22,6 +22,7 @@ module Isets { /* If all elements in iset x are in iset y, x is a subset of y. */ lemma LemmaSubset(x: iset, y: iset) + /* Dafny selected triggers: {e in y}, {e in x} */ requires forall e {:trigger e in y} :: e in x ==> e in y ensures x <= y { @@ -30,9 +31,10 @@ module Isets { /* Map an injective function to each element of an iset. */ function {:opaque} Map(xs: iset, f: X-->Y): (ys: iset) reads f.reads - requires forall x {:trigger f.requires(x)} :: f.requires(x) + requires forall x :: f.requires(x) requires Injective(f) - ensures forall x {:trigger f(x)} :: x in xs <==> f(x) in ys + /* Dafny selected triggers: {f(x)}, {x in xs} */ + ensures forall x {:trigger f(x)} :: x in xs <==> f(x) in ys { var ys := iset x | x in xs :: f(x); ys @@ -42,7 +44,8 @@ module Isets { returns true. */ function {:opaque} Filter(xs: iset, f: X~>bool): (ys: iset) reads f.reads - requires forall x {:trigger f.requires(x)} {:trigger x in xs} :: x in xs ==> f.requires(x) + requires forall x :: x in xs ==> f.requires(x) + /* Dafny selected triggers: {f(y)}, {y in xs}, {y in ys} */ ensures forall y {:trigger f(y)}{:trigger y in xs} :: y in ys <==> y in xs && f(y) { var ys := iset x | x in xs && f(x); diff --git a/src/Collections/Sets/Sets.dfy b/src/Collections/Sets/Sets.dfy index ae4058d6..8727a093 100644 --- a/src/Collections/Sets/Sets.dfy +++ b/src/Collections/Sets/Sets.dfy @@ -22,6 +22,7 @@ module Sets { /* If all elements in set x are in set y, x is a subset of y. */ lemma LemmaSubset(x: set, y: set) + /* Dafny selected triggers: {e in y}, {e in x} */ requires forall e {:trigger e in y} :: e in x ==> e in y ensures x <= y { @@ -80,10 +81,11 @@ module Sets { /* If an injective function is applied to each element of a set to construct another set, the two sets have the same size. */ lemma LemmaMapSize(xs: set, ys: set, f: X-->Y) - requires forall x {:trigger f.requires(x)} :: f.requires(x) + requires forall x :: f.requires(x) requires Injective(f) + /* Dafny selected triggers: {f(x)}, {x in xs} */ requires forall x {:trigger f(x)} :: x in xs <==> f(x) in ys - requires forall y {:trigger y in ys} :: y in ys ==> exists x :: x in xs && y == f(x) + requires forall y :: y in ys ==> exists x :: x in xs && y == f(x) ensures |xs| == |ys| { if xs != {} { @@ -97,8 +99,9 @@ module Sets { /* Map an injective function to each element of a set. */ function method {:opaque} Map(xs: set, f: X-->Y): (ys: set) reads f.reads - requires forall x {:trigger f.requires(x)} :: f.requires(x) + requires forall x :: f.requires(x) requires Injective(f) + /* Dafny selected triggers: {f(x)}, {x in xs} */ ensures forall x {:trigger f(x)} :: x in xs <==> f(x) in ys ensures |xs| == |ys| { @@ -111,7 +114,8 @@ module Sets { function returns true, the size of ys is less than or equal to the size of xs. */ lemma LemmaFilterSize(xs: set, ys: set, f: X~>bool) - requires forall x {:trigger f.requires(x)}{:trigger x in xs} :: x in xs ==> f.requires(x) + requires forall x :: x in xs ==> f.requires(x) + /* Dafny selected triggers: {f(y)}, {y in xs}, {y in ys} */ requires forall y {:trigger f(y)}{:trigger y in xs} :: y in ys ==> y in xs && f(y) ensures |ys| <= |xs| decreases xs, ys @@ -128,7 +132,8 @@ module Sets { true. */ function method {:opaque} Filter(xs: set, f: X~>bool): (ys: set) reads f.reads - requires forall x {:trigger f.requires(x)} {:trigger x in xs} :: x in xs ==> f.requires(x) + requires forall x :: x in xs ==> f.requires(x) + /* Dafny selected triggers: {f(y)}, {y in xs}, {y in ys} */ ensures forall y {:trigger f(y)}{:trigger y in xs} :: y in ys <==> y in xs && f(y) ensures |ys| <= |xs| { @@ -162,7 +167,7 @@ module Sets { /* Construct a set with all integers in the range [a, b). */ function method {:opaque} SetRange(a: int, b: int): (s: set) requires a <= b - ensures forall i {:trigger i in s} :: a <= i < b <==> i in s + ensures forall i :: a <= i < b <==> i in s ensures |s| == b - a decreases b - a { @@ -172,7 +177,7 @@ module Sets { /* Construct a set with all integers in the range [0, n). */ function method {:opaque} SetRangeZeroBound(n: int): (s: set) requires n >= 0 - ensures forall i {:trigger i in s} :: 0 <= i < n <==> i in s + ensures forall i :: 0 <= i < n <==> i in s ensures |s| == n { SetRange(0, n) @@ -181,12 +186,12 @@ module Sets { /* If a set solely contains integers in the range [a, b), then its size is bounded by b - a. */ lemma LemmaBoundedSetSize(x: set, a: int, b: int) - requires forall i {:trigger i in x} :: i in x ==> a <= i < b + requires forall i :: i in x ==> a <= i < b requires a <= b ensures |x| <= b - a { var range := SetRange(a, b); - forall e {:trigger e in range}{:trigger e in x} | e in x + forall e | e in x ensures e in range; { } From 85e585f824ae387bd7a1b305b56c2c76ca136173 Mon Sep 17 00:00:00 2001 From: yizhou7 Date: Thu, 14 Oct 2021 19:09:04 -0400 Subject: [PATCH 2/8] address some comments from @parno --- src/Collections/Sequences/Seq.dfy | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 4e425b24..1d31e649 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -267,7 +267,7 @@ module Seq { requires pos < |s| ensures |s'| == |s| - 1 ensures forall i | 0 <= i < pos :: s'[i] == s[i] - ensures forall i| pos <= i < |s| - 1 :: s'[i] == s[i+1] + ensures forall i | pos <= i < |s| - 1 :: s'[i] == s[i+1] { s[..pos] + s[pos+1..] } @@ -374,8 +374,7 @@ module Seq { requires 0 < |a| && 0 < |b| ensures Max(a+b) >= Max(a) ensures Max(a+b) >= Max(b) - /* Dafny selected trigger: {i in a + b} */ - ensures forall i {:trigger i in [Max(a + b)]} :: i in a + b ==> Max(a + b) >= i + ensures forall i :: i in a + b ==> Max(a + b) >= i { reveal Max(); if |a| == 1 { @@ -401,8 +400,7 @@ module Seq { requires 0 < |a| && 0 < |b| ensures Min(a+b) <= Min(a) ensures Min(a+b) <= Min(b) - /* Dafny selected trigger: {i in a + b} */ - ensures forall i {:trigger i in a + b} :: i in a + b ==> Min(a + b) <= i + ensures forall i :: i in a + b ==> Min(a + b) <= i { reveal Min(); if |a| == 1 { From 16c9e3db2e0173b0c5df637e121fec0dfbf27a51 Mon Sep 17 00:00:00 2001 From: yizhou7 Date: Thu, 14 Oct 2021 19:19:52 -0400 Subject: [PATCH 3/8] refomat some code, add some explainations on triggers --- STYLE.md | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/STYLE.md b/STYLE.md index c9ab1b5c..365698b8 100644 --- a/STYLE.md +++ b/STYLE.md @@ -7,30 +7,33 @@ This style guide provides coding conventions for the Dafny Standard Library code ## Naming Convention Any **variables** are named with `camelCase`. - +``` var minValue := 1; var cipherMessage := "Hello World"; - +``` Any **lemmas**, **predicates**, **functions**, **methods**, **classes**, **modules**, **datatypes**, and **newtypes** are named with `PascalCase`. - +``` method FindIndex(arr: seq, k: int) ... - +``` The **lemma** keyword indicates a ghost method used for proof purposes. Any **lemma** names should be prefixed with `Lemma`. - +``` lemma LemmaValueIsInIndex(arr: seq, k: int) ... +``` Any static or global **constants** are named with `UPPERCASE_WITH_UNDERSCORES`. - +``` static const MONTHS_IN_A_YEAR := 12 +``` ### Method Prefix Avoid redundant names when variables or methods are in a class/module. +``` class Integer { // The following method converts the given integer @@ -48,7 +51,7 @@ class Integer { method IntegerToString(i: int) returns (s: string) ... } - +``` ## Code Layout ### Braces @@ -77,14 +80,16 @@ module M { ### Imports By default, import modules without opening them. - +``` import Coffee ... +``` However, if some members of a module are used very frequently, import it using `opened`: - +``` import opened Donut ... +``` When a file uses two modules and both of them define a method of the same name, do not import them `opened`. @@ -369,3 +374,7 @@ lemma LemmaMyLemma ( x : seq> , y :B){ ... } ``` + +### Triggers + +The `{:trigger}` annotations used in the standard library are an advanced topic and should not be needed when starting out on Dafny projects. For some background on quantifiers and triggers, checkout [this](https://github.com/dafny-lang/dafny/wiki/FAQ#how-does-dafny-handle-quantifiers-ive-heard-about-triggers-what-are-those). \ No newline at end of file From b7ae16c36f5fcf78016a27d6ff43b456858bba03 Mon Sep 17 00:00:00 2001 From: yizhou7 Date: Thu, 14 Oct 2021 19:29:16 -0400 Subject: [PATCH 4/8] Update STYLE.md --- STYLE.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/STYLE.md b/STYLE.md index 365698b8..812a45b1 100644 --- a/STYLE.md +++ b/STYLE.md @@ -377,4 +377,4 @@ lemma LemmaMyLemma ( x : seq> , y :B){ ### Triggers -The `{:trigger}` annotations used in the standard library are an advanced topic and should not be needed when starting out on Dafny projects. For some background on quantifiers and triggers, checkout [this](https://github.com/dafny-lang/dafny/wiki/FAQ#how-does-dafny-handle-quantifiers-ive-heard-about-triggers-what-are-those). \ No newline at end of file +The `{:trigger}` annotations used in the standard library are an advanced topic and should not be needed when starting out on Dafny projects. For some background on quantifiers and triggers, check [this](https://github.com/dafny-lang/dafny/wiki/FAQ#how-does-dafny-handle-quantifiers-ive-heard-about-triggers-what-are-those) out. From 693707105fdad8ad43df8e9f97d439c9bcd7dd71 Mon Sep 17 00:00:00 2001 From: yizhou7 Date: Sat, 6 Nov 2021 16:13:30 -0400 Subject: [PATCH 5/8] remove trigger from pre-condition --- src/Collections/Sets/Isets.dfy | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Collections/Sets/Isets.dfy b/src/Collections/Sets/Isets.dfy index 64334646..d5ec31e5 100644 --- a/src/Collections/Sets/Isets.dfy +++ b/src/Collections/Sets/Isets.dfy @@ -22,8 +22,7 @@ module Isets { /* If all elements in iset x are in iset y, x is a subset of y. */ lemma LemmaSubset(x: iset, y: iset) - /* Dafny selected triggers: {e in y}, {e in x} */ - requires forall e {:trigger e in y} :: e in x ==> e in y + requires forall e :: e in x ==> e in y ensures x <= y { } From 064984bfceab33dc2b03160dfacdfa380347495c Mon Sep 17 00:00:00 2001 From: yizhou7 Date: Sat, 6 Nov 2021 16:19:07 -0400 Subject: [PATCH 6/8] update Reverse post condition trigger --- src/Collections/Sequences/Seq.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 1d31e649..0ccf08b5 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -303,12 +303,12 @@ module Seq { function method {:opaque} Reverse(s: seq): (s': seq) ensures |s'| == |s| - /* Dafny selected triggers: {s'[i]} */ - ensures forall i {:trigger s'[i]}{:trigger s[|s| - i - 1]} :: 0 <= i < |s| ==> s'[i] == s[|s| - i - 1] + ensures forall i :: 0 <= i < |s| ==> s'[i] == s[|s| - i - 1] + ensures forall i :: 0 <= i < |s| ==> s[i] == s'[|s|' - i - 1] { if s == [] then [] else [s[|s|-1]] + Reverse(s[0 .. |s|-1]) } - + function method {:opaque} Repeat(v: T, length: nat): (s: seq) ensures |s| == length ensures forall i: nat | i < |s| :: s[i] == v From 381bc75d12aebd3622c97a8ed5adf878f9ef8b28 Mon Sep 17 00:00:00 2001 From: yizhou7 Date: Sat, 6 Nov 2021 16:29:01 -0400 Subject: [PATCH 7/8] rename Union operations --- src/Collections/Maps/Imaps.dfy | 5 +++-- src/Collections/Maps/Maps.dfy | 9 +++++---- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/Collections/Maps/Imaps.dfy b/src/Collections/Maps/Imaps.dfy index 9a533bf0..c03f3e00 100644 --- a/src/Collections/Maps/Imaps.dfy +++ b/src/Collections/Maps/Imaps.dfy @@ -61,8 +61,9 @@ module Imaps { } /* Union of two imaps. Does not require disjoint domains; on the intersection, - values from the second imap are chosen. */ - function {:opaque} Union(m: imap, m': imap): (r: imap) + values from the second imap are chosen. PartiallyOpaqueUnion has more + restrictive triggers than +. */ + function {:opaque} PartiallyOpaqueUnion(m: imap, m': imap): (r: imap) ensures r.Keys == m.Keys + m'.Keys /* Dafny selected triggers: {m'[x]}, {r[x]}, {x in m'} */ ensures forall x {:trigger r[x]} :: x in m' ==> r[x] == m'[x] diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy index 12f85fec..dc1c56d1 100644 --- a/src/Collections/Maps/Maps.dfy +++ b/src/Collections/Maps/Maps.dfy @@ -73,8 +73,9 @@ module Maps { } /* Union of two maps. Does not require disjoint domains; on the intersection, - values from the second map are chosen. */ - function method {:opaque} Union(m: map, m': map): (r: map) + values from the second map are chosen. PartiallyOpaqueUnion has more + restrictive triggers than +. */ + function method {:opaque} PartiallyOpaqueUnion(m: map, m': map): (r: map) ensures r.Keys == m.Keys + m'.Keys /* Dafny selected triggers: {m'[x]}, {r[x]}, {x in m'} */ ensures forall x {:trigger r[x]} :: x in m' ==> r[x] == m'[x] @@ -88,9 +89,9 @@ module Maps { sizes. */ lemma LemmaDisjointUnionSize(m: map, m': map) requires m.Keys !! m'.Keys - ensures |Union(m, m')| == |m| + |m'| + ensures |PartiallyOpaqueUnion(m, m')| == |m| + |m'| { - var u := Union(m, m'); + var u := PartiallyOpaqueUnion(m, m'); assert |u.Keys| == |m.Keys| + |m'.Keys|; } From 9198630aed08f07482d8bce1433c6e1ddbf87129 Mon Sep 17 00:00:00 2001 From: yizhou7 Date: Mon, 8 Nov 2021 00:29:17 -0500 Subject: [PATCH 8/8] remove manual trigger for Injective/Monotonic/MonotonicFrom --- src/Collections/Maps/Imaps.dfy | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/Collections/Maps/Imaps.dfy b/src/Collections/Maps/Imaps.dfy index c03f3e00..30bb6247 100644 --- a/src/Collections/Maps/Imaps.dfy +++ b/src/Collections/Maps/Imaps.dfy @@ -76,8 +76,7 @@ module Imaps { /* True iff an imap is injective. */ predicate {:opaque} Injective(m: imap) { - /* Dafny selected triggers: {m[x'], m[x]}, {m[x'], x in m}, {m[x], x' in m}, {x' in m, x in m} */ - forall x, x' {:trigger m[x], m[x']} :: x != x' && x in m && x' in m ==> m[x] != m[x'] + forall x, x' :: x != x' && x in m && x' in m ==> m[x] != m[x'] } /* Swaps imap keys and values. Values are not required to be unique; no @@ -105,16 +104,13 @@ module Imaps { /* True iff an imap is monotonic. */ predicate {:opaque} Monotonic(m: imap) { - /* Dafny selected triggers: {m[x'], m[x]}, {m[x'], x in m}, {m[x], x' in m}, {x' in m, x in m} */ - forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && x <= x' ==> m[x] <= m[x'] + forall x, x' :: x in m && x' in m && x <= x' ==> m[x] <= m[x'] } /* True iff an imap is monotonic. Only considers keys greater than or equal to start. */ predicate {:opaque} MonotonicFrom(m: imap, start: int) { - /* Dafny selected triggers: {m[x'], m[x]}, {m[x'], x in m}, {m[x], x' in m}, {x' in m, x in m} */ - forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && start <= x <= x' ==> m[x] <= m[x'] + forall x, x' :: x in m && x' in m && start <= x <= x' ==> m[x] <= m[x'] } - }