594 questions
1
vote
1
answer
107
views
How do I help dafny see the obvious here?
Obviously, the set of nonnegative integers below n has cardinality n. But dafny seemingly can't prove it:
method FirstNonnegatives(n: nat) returns (s: set<nat>)
ensures |s| == n
{
s := ...
- 182
1
vote
1
answer
78
views
Array Reverse Proof by Dafny
Regarding the array reversal problem, I guess loop invariants are logically correct, based on the symmetry of the elements in the array and their relationship after reversal.
However, I don’t ...
- 13
0
votes
0
answers
31
views
Higher-order identity function does not verify because precondition of f.reads cannot be proved
I am playing with higher-order functions in Dafny. I am specifically interested in functions that work with partial and heap-reading functions (i.e. of the general type A ~> B). The issues I ran ...
- 2,809
1
vote
1
answer
91
views
Dafny module system and refinement: sharing an underlying type across diferent abstract modules
I want to know if it is possible to achieve something (at least similar) to the following:
abstract module A {
type T
function f(x:T) : nat // A's operations on T
}
abstract module B {
type ...
- 5,488
1
vote
2
answers
65
views
Trying to prove the multiset of a sequence is equal to the multiset of that sequence broken up
I'm having trouble proving this within a while loop in Dafny:
assert multiset(seqa) == multiset(seqa[..i] + seqa[i..]);
Note:
An invariant exists ensuring that 0 <= i <= |seqa|.
There are no ...
- 11
1
vote
1
answer
76
views
Framing verification issue on mutable array in a typical ArrayList Insert operation
Consider the following simple ArrayList implementation:
class ArrayListImpl<T(0)> {
var xs: array<T>
var n: nat
predicate Valid() reads this
{ 0 <= n <= xs.Length }
...
- 5,488
2
votes
1
answer
78
views
Why does Dafny fails to verify this simple code?
I'm trying to prove certain properties of integer lists hold.
To begin with it, I wrote method Check1 below, utilizing a method given by CoPilot.
method FlipSeq(s: seq<int>) returns (res: seq<...
1
vote
1
answer
63
views
Indexing array by bv32 in Dafny causes timeout
ghost predicate AllZero(a: array<int>, n: bv32)
reads a {
a.Length == (n as int) &&
(forall i :: 0 <= i < n ==> a[i] == 0)
}
I need to use the result of binary ...
- 63
0
votes
1
answer
54
views
How to prove the loop invariant of Mergesort with Frama-C WP
I'm attempting to annotate the merge sort algorithm with ACSL specifications and verify its correctness using Frama-C's WP plugin, but I'm running into some issues. Below is my code:
/*@
predicate ...
- 51
2
votes
2
answers
58
views
Frama-C WP unable to prove postcondition of function LinearSearch
I am attempting to add ACSL annotations to some classic algorithms from Introduction to Algorithms and verify their correctness using Frama-C's WP plugin, but I have encountered some issues.
Here is ...
- 51
1
vote
3
answers
99
views
Why does Dafny verify this?
I apologize for the somewhat vague question title -- I honestly don't know how to ask this more precisely.
Why does the following code verify?
ghost function {:axiom} max(a: int, b: int) : int
...
- 71
1
vote
1
answer
93
views
Real number equality in Dafny: proving x^2 is positive for x > 0
I came across the following strange example of real number equality in Dafny, after a student pointed me to a related issue.
First, when we have two real numbers that are equal, and one of them is ...
- 534
-1
votes
2
answers
79
views
Why is this lemma not automatically proved in dafny? How to prove it by hand?
In simple words:
If A and B are equivalent multisets, then elements not in A are not in B as well.
lemma ElementExclusionLemma<T>(seqa: seq<T>, seqb: seq<T>, x: T)
ensures multiset(...
- 13
1
vote
2
answers
55
views
Dafny verifier fails to prove the consequence of multiset
I'm working with Dafny and trying to understand how specifications, particularly modifies and ensures multiset, affect verification.
I have a method do_nothing which is specified to modify an array a ...
- 13
2
votes
1
answer
98
views
Quantifier introduction in Dafny: prove abs is surjective
This is a similar question but I haven't been able to map it to my use case.
Basically I want to use Dafny to prove a basic statement with nested quantifiers (for all X there exists Y) in first-order ...
- 534