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

Jump to bottom

Add the axiom stating that Seq#Take(s, Seq#Length(s)) == s) for all… #4195

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

Add the axiom stating that Seq#Take(s, Seq#Length(s)) == s) for all… #4195

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
862e5f7
Add the axiom stating that `Seq#Take(s, Seq#Length(s)) == s)` for all…
btwael Jun 19, 2023
68781d8
Update Test/git-issues/git-issue-4184.dfy
MikaelMayer Jun 19, 2023
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
Next Next commit
Add the axiom stating that Seq#Take(s, Seq#Length(s)) == s) for all… 
… sequence `s` (#4194)

A trivial axiom stating `Seq#Take(s, Seq#Length(s)) == s)` for all
sequence `s`. This will help deducing automatically and without using
any workaround that "multiset(arr[..]) == multiset(arr[..arr.Length])"
for any array `arr`.

Fixes #4184

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
@btwael
btwael committed Jun 19, 2023
commit 862e5f79b47f6e4c4ebeab183a81c07836f63b17
4 changes: 4 additions & 0 deletions Source/DafnyCore/DafnyPrelude.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1106,6 +1106,10 @@ axiom (forall<T> s, t: Seq T, n: int ::
Seq#Take(Seq#Append(s, t), n) == s &&
Seq#Drop(Seq#Append(s, t), n) == t);

axiom (forall<T> s : Seq T ::
{ Seq#Take(s, Seq#Length(s)) }
Seq#Take(s, Seq#Length(s)) == s);

function Seq#FromArray(h: Heap, a: ref): Seq Box;
axiom (forall h: Heap, a: ref ::
{ Seq#Length(Seq#FromArray(h,a)) }
Expand Down
7 changes: 7 additions & 0 deletions Test/git-issues/git-issue-4184.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
// RUN: %baredafny verify %args "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

method main() {
var arr: array<int>;
MikaelMayer marked this conversation as resolved.
Show resolved Hide resolved
assert(multiset(arr[..]) == multiset(arr[..arr.Length]));
}
2 changes: 2 additions & 0 deletions Test/git-issues/git-issue-4184.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@

Dafny program verifier finished with 1 verified, 0 errors
Loading