165 questions
- Bountied 0
- Unanswered
- Frequent
- Score
- Trending
- Week
- Month
- Unanswered (my tags)
1
vote
1
answer
152
views
Dafny loop invariant troubles
I've started learning Dafny recently, and I can't really get my head around creating loop invariants.
The following is a method which aims to change a given integer array such that where possible a[i] ...
0
votes
1
answer
43
views
Does loop invariant verification using SMTs require enumerating values of variables?
I am trying to understand how loop invariant verification conditions work, particularly in the context of SMT solvers. Consider the following simple loop:
i = 0
while i < 10:
i += 1
Suppose I ...
0
votes
2
answers
219
views
How do I infer the weakest precondition when a loop invariant is given?
I previously asked this question on StackOverflow about using loop invariants to catch a bug in my program. Now, I want to take the next step and understand how to compute the weakest precondition ...
0
votes
2
answers
85
views
Can't solve this Dafny problem about implementing a O(n) algorithm
predicate Asc(a: array<int>)
reads a
{
forall i,j:: 0<=i<j<a.Length ==> a[i] <= a[j]
}
method occursInBoth(a: array<int>, b: array<int>) returns (r : bool)
...
0
votes
2
answers
72
views
Why is this Dafny Method not holding when it should?
method search(a: array<int>) returns (i : int)
requires a.Length > 1 && a[0] == a[a.Length-1]
ensures 0 <= i < a.Length-1 && a[i] >= a[i + 1]
{
i := ......;
...
0
votes
1
answer
101
views
Dafny method does not verify
I have a method that returns the lowest index of the first bad neighbour or -1 if there are none.
If a neighbouring pair of elements have a negative sum then the right neighbour is said to be bad. For ...
0
votes
1
answer
65
views
About Dafny loop invariant errors
The following code is the answer I came up with for the following problem. However, there are two main errors. By the way, this problem is problem 17 in Chapter 13 of the book "PROGRAM PROOFS&...
0
votes
1
answer
181
views
Dafny Loop Invariant
I was writing code for a loop-based square root estimation method in Dafny, this is what I have:
method sqrt(val :int) returns (root:int)
requires val >= 0
ensures root * root >= val && (...
-2
votes
2
answers
238
views
how can i remove loop invariant in this [closed]
In the code below i have to remove all loop-invariant computations, my friend has given me this problem and I am not able to solve it for a long time.
x = 10
a = 20
for(i = 0;i<10;i++){
b = a * ...
1
vote
1
answer
277
views
cannot prove function in frama-C
I am having a problem regarding the function proving in frama C. my code used for proving looks like this :
#include <limits.h>
/*@
requires len>=0 && \valid(arr + (0 .. len-1));
...
1
vote
1
answer
597
views
Insertion Sort Loop Invariant : Maintenance
I am reading loop invariant for insertion sort from the book Introduction to Algorithm by CLRS.
Pseudo code for the insertion sort is:
1 for i = 2 to n
2 key = A[i]
3 // Insert A[i] into the ...
1
vote
1
answer
155
views
Proving non-linear traversal terminates in Dafny
I have an array of nats in Dafny that I want to traverse in a non-linear manner. To elucidate the problem: Consider an array such that (please ignore the syntax for now):
var links : array<nat>;
...
1
vote
1
answer
295
views
Dafny method will not verify
I have this method that returns the number of trailing zeros, and modifies the array a to replace all the trailing zeros with -1. Currently I am getting assertion might not hold error on assert s == 1 ...
0
votes
1
answer
700
views
Calculating integer exponents in dafny
I'm new to dafny and I am having trouble with getting exponents for integers
invariant x >= 0 && y >= 0 && ((x + y) * (2^(u-1)) + result == i1 + i2);
for the part that says "...
0
votes
0
answers
140
views
Can parameters depend on a parameter in a loop invariant in ada?
Please can you tell me whether or not the parameters (in or out or in out) and the depends clause, are correct for the rest of the program.
Question: I am unsure if the loop invariant can 'use' a ...