forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'coverage-report-per-module-breakdown' of github.com:rob…
…in-aws/dafny into per-backend-code-support-in-stdlibs # Conflicts: # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-arithmetic.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo
- Loading branch information
Showing
18 changed files
with
1,758 additions
and
14 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Binary file modified
BIN
+0 Bytes
(100%)
Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-arithmetic.doo
Binary file not shown.
Binary file modified
BIN
+6.69 KB
(170%)
Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
41 changes: 41 additions & 0 deletions
41
Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Arrays.dfy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,41 @@ | ||
| /******************************************************************************* | ||
| * Copyright by the contributors to the Dafny Project | ||
| * SPDX-License-Identifier: MIT | ||
| *******************************************************************************/ | ||
|
|
||
| /** | ||
| This module defines useful properties and functions relating to the built-in `array` type. | ||
| */ | ||
| module DafnyStdLibs.Collections.Arrays { | ||
|
|
||
| import opened Wrappers | ||
| import opened Relations | ||
| import opened Seq | ||
|
|
||
| method BinarySearch<T>(a: array<T>, key: T, less: (T, T) -> bool) returns (r: Option<nat>) | ||
| requires Seq.SortedBy(a[..], (x, y) => less(x, y) || x == y) | ||
| requires StrictTotalOrdering(less) | ||
| ensures r.Some? ==> r.value < a.Length && a[r.value] == key | ||
| ensures r.None? ==> key !in a[..] | ||
| { | ||
| var lo, hi : nat := 0, a.Length; | ||
| while lo < hi | ||
| invariant 0 <= lo <= hi <= a.Length | ||
| invariant key !in a[..lo] && key !in a[hi..] | ||
| invariant a[..] == old(a[..]) | ||
| { | ||
| var mid := (lo + hi) / 2; | ||
|
|
||
| if less(key, a[mid]) { | ||
| hi := mid; | ||
| } else if less(a[mid], key) { | ||
| lo:= mid + 1; | ||
| } else { | ||
| return Some(mid); | ||
| } | ||
| } | ||
|
|
||
| return None; | ||
| } | ||
|
|
||
| } |
13 changes: 13 additions & 0 deletions
13
Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Collections.dfy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| /******************************************************************************* | ||
| * Copyright by the contributors to the Dafny Project | ||
| * SPDX-License-Identifier: MIT | ||
| *******************************************************************************/ | ||
|
|
||
| /** | ||
| This module contains submodules each defining useful properties and functions | ||
| relating to the built-in collection types. | ||
| */ | ||
| module DafnyStdLibs.Collections { | ||
| // This module currently contains no definitions, | ||
| // but is defined so that the module comment appears in generated documentation. | ||
| } |
27 changes: 27 additions & 0 deletions
27
Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Collections.md
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,27 @@ | ||
| ## The `Collections` module | ||
|
|
||
| This module includes a variety of submodules that define properties of | ||
| various collections: | ||
|
|
||
| - Sets: functions and lemmas expressing properties of Dafny's `set<T>` type, such as properties of subsets, unions, and intersections, filtering of sets using predicates, mapping sets to other sets using functions | ||
|
|
||
| - Isets: function and lemmas to manipulate `iset`s | ||
|
|
||
| - Seqs: functions and lemmas expressing properties of Dafny's `seq<T>` type, | ||
| such as properties of subsequences, filtering of sequences, | ||
| finding elements (i.e., index-of, last-index-of), | ||
| inserting or removing elements, | ||
| reversing, repeating or combining (zipping or flattening) sequences, | ||
| sorting, and | ||
| conversion to sets. | ||
|
|
||
| - Maps: functions and lemmas to manipulate `map`s | ||
|
|
||
| - Imaps: functions and lemmas to manipulate `imap`s | ||
|
|
||
| - Arrays: manipulations of arrays | ||
|
|
||
| <!-- TODO | ||
| - LittleEndianNat: properties of sequences that represent natural numbers expressed as a given base, with the least significant digit at position 0 of the sequence and each element in the range 0 to the base. | ||
| - LittleEndianNatConversions: conversions between two little-endian representations of nats in different bases | ||
| --> |
109 changes: 109 additions & 0 deletions
109
Source/DafnyStandardLibraries/src/DafnyStdLibs/Collections/Imaps.dfy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,109 @@ | ||
| /******************************************************************************* | ||
| * Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, | ||
| * ETH Zurich, and University of Washington | ||
| * SPDX-License-Identifier: BSD-2-Clause | ||
| * | ||
| * Modifications and Extensions: Copyright by the contributors to the Dafny Project | ||
| * SPDX-License-Identifier: MIT | ||
| *******************************************************************************/ | ||
|
|
||
| /** | ||
| This module defines useful properties and functions relating to the built-in `imap` type. | ||
| */ | ||
| module DafnyStdLibs.Collections.Imaps { | ||
|
|
||
| import opened Wrappers | ||
|
|
||
| function Get<X, Y>(m: imap<X, Y>, x: X): Option<Y> | ||
| { | ||
| if x in m then Some(m[x]) else None | ||
| } | ||
|
|
||
| /* Remove all key-value pairs corresponding to the iset of keys provided. */ | ||
| ghost function {:opaque} RemoveKeys<X, Y>(m: imap<X, Y>, xs: iset<X>): (m': imap<X, Y>) | ||
| ensures forall x {:trigger m'[x]} :: x in m && x !in xs ==> x in m' && m'[x] == m[x] | ||
| ensures forall x {:trigger x in m'} :: x in m' ==> x in m && x !in xs | ||
| ensures m'.Keys == m.Keys - xs | ||
| { | ||
| imap x | x in m && x !in xs :: m[x] | ||
| } | ||
|
|
||
| /* Remove a key-value pair. Returns unmodified imap if key is not found. */ | ||
| ghost function {:opaque} RemoveKey<X, Y>(m: imap<X, Y>, x: X): (m': imap<X, Y>) | ||
| ensures m' == RemoveKeys(m, iset{x}) | ||
| ensures forall x' {:trigger m'[x']} :: x' in m' ==> m'[x'] == m[x'] | ||
| { | ||
| imap i | i in m && i != x :: m[i] | ||
| } | ||
|
|
||
| /* Keep all key-value pairs corresponding to the iset of keys provided. */ | ||
| ghost function {:opaque} Restrict<X, Y>(m: imap<X, Y>, xs: iset<X>): (m': imap<X, Y>) | ||
| ensures m' == RemoveKeys(m, m.Keys - xs) | ||
| { | ||
| imap x | x in xs && x in m :: m[x] | ||
| } | ||
|
|
||
| /* True iff x maps to the same value or does not exist in m and m'. */ | ||
| ghost predicate EqualOnKey<X, Y>(m: imap<X, Y>, m': imap<X, Y>, x: X) | ||
| { | ||
| (x !in m && x !in m') || (x in m && x in m' && m[x] == m'[x]) | ||
| } | ||
|
|
||
| /* True iff m is a subset of m'. */ | ||
| ghost 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) | ||
| } | ||
|
|
||
| /* Union of two imaps. Does not require disjoint domains; on the intersection, | ||
| values from the second imap are chosen. */ | ||
| ghost function {:opaque} Union<X, Y>(m: imap<X, Y>, m': imap<X, Y>): (r: imap<X, Y>) | ||
| ensures r.Keys == m.Keys + m'.Keys | ||
| ensures forall x {:trigger r[x]} :: x in m' ==> r[x] == m'[x] | ||
| ensures forall x {:trigger r[x]} :: x in m && x !in m' ==> r[x] == m[x] | ||
| { | ||
| m + m' | ||
| } | ||
|
|
||
| /* True iff an imap is injective. */ | ||
| ghost 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'] | ||
| } | ||
|
|
||
| /* Swaps imap keys and values. Values are not required to be unique; no | ||
| promises on which key is chosen on the intersection. */ | ||
| ghost function {:opaque} Invert<X, Y>(m: imap<X, Y>): imap<Y, X> | ||
| { | ||
| imap y | y in m.Values :: var x :| x in m.Keys && m[x] == y; x | ||
| } | ||
|
|
||
| /* Inverted maps are injective. */ | ||
| lemma LemmaInvertIsInjective<X, Y>(m: imap<X, Y>) | ||
| ensures Injective(Invert(m)) | ||
| { | ||
| reveal Injective(); | ||
| reveal Invert(); | ||
| } | ||
|
|
||
| /* True iff an imap contains all valid keys. */ | ||
| ghost predicate {:opaque} Total<X(!new), Y>(m: imap<X, Y>) | ||
| { | ||
| forall i {:trigger m[i]}{:trigger i in m} :: i in m | ||
| } | ||
|
|
||
| /* True iff an imap is monotonic. */ | ||
| ghost 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'] | ||
| } | ||
|
|
||
| /* True iff an imap is monotonic. Only considers keys greater than or | ||
| equal to start. */ | ||
| ghost 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'] | ||
| } | ||
|
|
||
| } |
Oops, something went wrong.