Dafny is a programming language with built-in specification constructs.
Dafny is a compiled language used for functional testing of functional correctness of programs.
Home page: https://dafny.org/
Questions tagged [dafny]
485 questions
23
votes
1 answer
what's the difference between lean, f*, and dafny?
They are from Microsoft and seem like they are proof assistants? Besides syntactical differences are there practical aspects that make them different from one another (say ability to do automation, expressive power, etc)? I am new to formal…
JRR
- 6,014
- 6
- 39
- 59
17
votes
1 answer
Proving the 100 Prisoners and a lightbulb with Dafny
Consider the standard strategy to solve the 100 prisoners and a lightbulb problem. Here's my attempt to model it in Dafny:
method strategy(P: set, Special: T) returns (count: int)
requires |P| > 1 && Special in P
ensures count == (|P| -…
Hugo Sereno Ferreira
- 8,600
- 7
- 46
- 92
7
votes
1 answer
Reading from (Writing to) files in Dafny
I've been looking at some dafny tutorials and couldn't find how to read from (or write to) simple text files. Surely, this has to be possible right?
OrenIshShalom
- 5,974
- 9
- 37
- 87
7
votes
1 answer
Dafny: What does no terms found to trigger on mean?
I am getting a warning in Dafny which says that my quantifiers have
No terms found to trigger on.
What I am trying to do for my code is to find the largest number that has a square value that is less than or equal to the given natural number 'n'.…
Chris
- 81
- 1
- 4
6
votes
1 answer
Dafny context modifies clause error
i am having a really hard time getting rid of the last error in my Dafny program. Can someone point me in the right direction?
Here is the code: http://rise4fun.com/Dafny/2FPo
I am getting this error: assignment may update an array element not in…
Adrien Pecher
- 335
- 1
- 7
- 14
5
votes
2 answers
How to make Pre and Post conditions for recursive functions in SPARK?
I'm translating an exercise I made in Dafny into SPARK, where one verifies a tail recursive function against a recursive one. The Dafny source (censored, because it might still be used for classes):
function Sum(n:nat):nat
decreases n
{
if…
Andreas
- 5,086
- 3
- 16
- 36
5
votes
1 answer
How to get a C# program from a dafny program?
I cannot see how to get a C# program from a dafny program.
I've downloaded dafny in Visual Studio Code and also downloaded C#. I have a program in dafny and can right-click on the program and choose Compile and Run, but I'd like to generate a C#…
LyX2394
- 121
- 1
- 5
4
votes
1 answer
Dafny: verify test case of array sorting with duplicates
Given the usual specification of array sorting in Dafny,
method sort(a: array)
modifies a
ensures isSorted(a[..])
ensures multiset(a[..]) == multiset(old(a[..]))
predicate isSorted(s: seq) {
forall i, j :: 0 <= i < j < |s| ==>…
João Pascoal Faria
- 41
- 2
4
votes
1 answer
While loop termination with null references in Dafny linked list implementation
I am new to Dafny and am trying to write a simple linked list implementation that adds all the integers stored in a linked list. Here is the code:
class Node {
var elem: int;
var next: Node?;
constructor (data: int)
{
elem := data;
next :=…
Johnny Green
- 43
- 2
4
votes
1 answer
Dafny difference between seq and array
I can't seem to tell the difference between dafny's seq and array.
Do they correspond to their SMT entities? (not sure because arrays in dafny have .Length)
OrenIshShalom
- 5,974
- 9
- 37
- 87
4
votes
1 answer
Dafny no terms to trigger on predicate
I have the following snippet Dafny code for a tic tac toe game to check if player 1 has a winning row on the board:
predicate isWinRowForPlayer1(board: array2)
reads board
requires board.Length0 == board.Length1 == 3 &&…
Jofbr
- 455
- 3
- 23
4
votes
1 answer
How do I iterate over the elements of a finite set object in Dafny?
What is the best way to iterate over the elements of a finite set object in Dafny? An example of working code would be delightful.
Kevin S
- 497
- 2
- 10
4
votes
1 answer
(Dafny) Adding elements of an array into another - loop invariant
I have a function sum that takes two arrays a and b as inputs and modifies b such that b[i] = a[0] + a[1] + ... + a[i]. I wrote this function and want to verify it with Dafny. However, Dafny tells me that my loop invariant might not be maintainted…
Dory
- 139
- 1
- 9
4
votes
2 answers
Can dafny show a counter example for a failed assertion?
I am trying to prove correctness / incorrectness of the following program using Dafny.
datatype List = Nil | Cons(T, List)
function tail(l:List):List
{
match l
case Nil => Nil
case Cons(x,xs) => xs
}
method check(l:List)
{
…
ankitrokdeonsns
- 638
- 4
- 18
4
votes
1 answer
Selection Sort in Dafny
I am trying to implement selection sort in Dafny.
My sorted and FindMin functions do work, but selectionsort itself contains assertions which Dafny will not prove, even if they are correct.
Here is my program:
predicate sorted(a:array,i:int)
…
hacatu
- 638
- 6
- 15