414 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
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
61
views
How to deal with potentially-aliased arguments in VST?
Consider the following code:
void incr(int *a, int *b) {
(*a)++;
(*b)++;
}
void f(int *a, int *b) {
incr(a, b);
incr(a, a);
}
The incr function admits two specifications:
{a ↦ n * b ↦ m}...
- 500
3
votes
2
answers
141
views
Problems proving trivial things involving shift operators using Frama-C WP
I have this very simple example.
/*@
requires a >= 0 && a <= 2;
assigns \nothing;
ensures \result < 10;
*/
int bob(int a) {
return 1 << a;
}
When I try to prove this ...
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
4
votes
1
answer
122
views
Frama-C / WP Proof of Moving Average Function - Pointer validity of array slice fails
I am learning about formal verification and using frama-c and the WP plug-in, and after reading some papers and following the WP Tutorial by Allan Blanchard, I decide to try to verify a function not ...
- 63
0
votes
0
answers
29
views
KeY prover failing to verify that swapping two elements of an array results in a permutation of the array
I am trying to prove a sorting algorithm, following the KeY textbook for reference (class SortPerm in chapter 16). I started with insertion sort but tried splitting it into multiple methods to make it ...
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
0
votes
0
answers
28
views
NuSMV - Issue with counter-based signal activation in Model
I have a project for the Embedded System Design course where I need to model a fault-tolerant sensor reading mechanism. I have reduce the system to only the important parts. The system relies on error ...
-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
197
views
Lean 4: Agda user struggling to understand Lean's equality type, type mismatch, not reducing
I am quite comfortable with Agda. I decided to experiment with Lean, but I find that propositional equality is really messing with me. Sometimes I find that rfl just works, but at other times it doesn'...
- 57
0
votes
1
answer
79
views
I cannot understand why Alloy does not find an instance for my model
I am trying to solve Halmos' handshake problem (Section 2.3) using Alloy 4 (I am required to use Alloy 4 for my university course; however this problem sheet is not part of my coursework, I am trying ...
- 1,840
2
votes
1
answer
113
views
Is Dafny 4.10 too powerful for exercises in Leino's book "Program proofs"?
I'm working through Leino's nice book "Program proofs" ((c) date 2023). The book is really well-written, explains thoroughly and progresses exactly as I need. But as I'm reproducing examples ...
- 71
1
vote
0
answers
71
views
Can you write a Linux kernel module that reclaims "in use" address space via a new syscall?
Motivation
I'm picturing a hypothetical update process for critical services, that might work like this (using C and POSIX names):
Download the new update binary, to a separate place than current ...
- 978