Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

some trigger updates #25

Open
wants to merge 8 commits into
base: master
Choose a base branch
from
Open

some trigger updates #25

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
7fe04f3
removed some tiggers that repeats dafny, added some comments for dafn…
yizhou7 Oct 10, 2021
85e585f
address some comments from @parno
yizhou7 Oct 14, 2021
16c9e3d
refomat some code, add some explainations on triggers
yizhou7 Oct 14, 2021
b7ae16c
Update STYLE.md
yizhou7 Oct 14, 2021
6937071
remove trigger from pre-condition
yizhou7 Nov 6, 2021
064984b
update Reverse post condition trigger
yizhou7 Nov 6, 2021
381bc75
rename Union operations
yizhou7 Nov 6, 2021
9198630
remove manual trigger for Injective/Monotonic/MonotonicFrom
yizhou7 Nov 8, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 18 additions & 9 deletions STYLE.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<int>, 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<int>, 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
Expand All @@ -48,7 +51,7 @@ class Integer {
method IntegerToString(i: int) returns (s: string)
...
}
```
## Code Layout

### Braces
Expand Down Expand Up @@ -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`.

Expand Down Expand Up @@ -369,3 +374,7 @@ lemma LemmaMyLemma <A,B> ( x : seq<seq<A>> , 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, check [this](https://github.com/dafny-lang/dafny/wiki/FAQ#how-does-dafny-handle-quantifiers-ive-heard-about-triggers-what-are-those) out.
20 changes: 13 additions & 7 deletions src/Collections/Maps/Imaps.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,9 @@ module Imaps {

/* Remove all key-value pairs corresponding to the iset of keys provided. */
function {:opaque} RemoveKeys<X, Y>(m: imap<X, Y>, xs: iset<X>): (m': imap<X, Y>)
/* 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
{
Expand All @@ -32,6 +34,7 @@ module Imaps {
/* Remove a key-value pair. Returns unmodified imap if key is not found. */
function {:opaque} RemoveKey<X, Y>(m: imap<X, Y>, x: X): (m': imap<X, Y>)
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]
Expand All @@ -54,14 +57,17 @@ module Imaps {
predicate IsSubset<X, Y>(m: imap<X, Y>, m': imap<X, Y>)
{
&& 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<X, Y>(m: imap<X, Y>, m': imap<X, Y>): (r: imap<X, Y>)
values from the second imap are chosen. PartiallyOpaqueUnion has more
restrictive triggers than +. */
function {:opaque} PartiallyOpaqueUnion<X, Y>(m: imap<X, Y>, m': imap<X, Y>): (r: imap<X, Y>)
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'
Expand All @@ -70,7 +76,7 @@ module Imaps {
/* True iff an imap is injective. */
predicate {:opaque} Injective<X, Y>(m: imap<X, Y>)
{
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
Expand All @@ -91,20 +97,20 @@ module Imaps {
/* True iff an imap contains all valid keys. */
predicate {:opaque} Total<X(!new), Y>(m: imap<X, Y>)
{
/* Dafny selected triggers: {i in m} */
forall i {:trigger m[i]}{:trigger i in m} :: i in m
yizhou7 marked this conversation as resolved.
Show resolved Hide resolved
}

/* True iff an imap is monotonic. */
predicate {:opaque} Monotonic(m: imap<int, int>)
{
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<int, int>, start: int)
{
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']
}

}
21 changes: 16 additions & 5 deletions src/Collections/Maps/Maps.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,15 +21,19 @@ module Maps {
}

function method {:opaque} ToImap<X, Y>(m: map<X, Y>): (m': imap<X, Y>)
/* 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]
}

/* Remove all key-value pairs corresponding to the set of keys provided. */
function method {:opaque} RemoveKeys<X, Y>(m: map<X, Y>, xs: set<X>): (m': map<X, Y>)
/* 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
Comment on lines +36 to 37
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The trigger in the other direction (that is, x in m) seems equally useful to me. Is there a reason not to include it?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since the ensures is an implication, we might only want the x in m'? My limited understanding is that we are ensuring the properties of m', rather than the original m. So might not be necessary to invoke this fact every time we see the original map.

ensures m'.Keys == m.Keys - xs
{
Expand Down Expand Up @@ -65,14 +69,17 @@ module Maps {
predicate IsSubset<X, Y>(m: map<X, Y>, m': map<X, Y>)
{
&& 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<X, Y>(m: map<X, Y>, m': map<X, Y>): (r: map<X, Y>)
values from the second map are chosen. PartiallyOpaqueUnion has more
restrictive triggers than +. */
function method {:opaque} PartiallyOpaqueUnion<X, Y>(m: map<X, Y>, m': map<X, Y>): (r: map<X, Y>)
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'
Expand All @@ -82,15 +89,16 @@ module Maps {
sizes. */
lemma LemmaDisjointUnionSize<X, Y>(m: map<X, Y>, m': map<X, Y>)
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|;
}

/* True iff a map is injective. */
predicate {:opaque} Injective<X, Y>(m: map<X, Y>)
{
/* 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']
}

Expand All @@ -112,19 +120,22 @@ module Maps {
/* True iff a map contains all valid keys. */
predicate {:opaque} Total<X(!new), Y>(m: map<X, Y>)
{
/* 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<int, 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 && x <= x' ==> m[x] <= m[x']
}

/* True iff a map is monotonic. Only considers keys greater than or
equal to start. */
predicate {:opaque} MonotonicFrom(m: map<int, int>, 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']
}

Expand Down
Loading