Boogie is an intermediate verification language created at Microsoft Research, intended as a layer on which to build program verifiers for other languages.
Questions tagged [boogie]
8 questions
3
votes
1 answer
What are triggers in Dafny/Boogie?
I have been limping along in Dafny without understanding triggers. Perhaps as a result, the programs I write seem to give the verifier a hard time. Sometimes I spend tons of time fiddling with my proof, trying to convince Dafny/Boogie that it's…
Jason Orendorff
- 42,793
- 6
- 62
- 96
2
votes
1 answer
What are the sources of non-robustness in Dafny proofs?
I occasionally (not frequently, but often enough) see it happen that a proof will be working in Dafny, and then something that appears irrelevant will change (e.g., variable names, function definition that aren't relevant to the proof, and so on)…
tjhance
- 961
- 1
- 7
- 14
2
votes
1 answer
How to read dafny counterexamples
I'd like to understand counterexamples produced by Dafny. I'm using the following code as an example:
function update_map(m1: map, m2: map): map
ensures
(forall k :: k in m1 || k in m2 ==> k in update_map(m1, m2)) &&
…
Samuel Gruetter
- 1,713
- 12
- 11
1
vote
1 answer
Can I find non-spurious counter example if I use different Boogie backend to check translated bpl files by Dafny?
As mentioned in the Wiki on Dafny GitHub, when Dafny cannot prove an assertion in a program, it might be due to either my program is incorrect OR the incompleteness of Dafny. But I figured the counter example from Dafny is spurious after I tried…
Chiao Hsieh
- 13
- 2
1
vote
0 answers
Logic error or Boogie bug? Quantifiers: exists of a forall
I'm working with the Boogie verification language, where I have the following example that gives a result that is counterintuitive to me.
// Defining a function and giving it a meaning through axiomatization.
function EqualsInt(x: int, y: int) :…
tyr.bentsen
- 143
- 1
- 6
0
votes
1 answer
Vectors vs Sequences in Boogie
Looking through the tests that come with Boogie, I noticed there are two collection types: Seq T and Vec T. Examples are:
type {:builtin "Seq"} Seq _;
function {:builtin "seq.empty"} empty(): Seq int;
function {:builtin "seq.len"} len(a: Seq int):…
redjamjar
- 535
- 2
- 11
0
votes
0 answers
Does random_seed affect the initial state of parameters in an implementation?
I'm interested in leveraging the random_seed attribute in order to have variety in the values returned by z3's counterexample. For instance, this implementation has 3 parameters of different types.
implementation {:random_seed N}…
twhatm9
- 27
- 4
0
votes
1 answer
Invariants and old() in Boogie
I'm verifying the following piece of code with boogie:
var v: int;
procedure main()
modifies v;
{
v := 0;
while(true)
invariant v > old(v) || v == 0;
{
v := v+1;
}
}
And the output is:
main2.bpl(10,9): Error:…
Patricio Inzaghi
- 131
- 11