Discussions under General

Comparing strings by (in)equality doesn't work

first post: jiplucap wrote: http://rise4fun.com/Dafny/SNDyT http://rise4fun.com/Dafny/19Sh I ...

latest post: rustanleino wrote: Fixed (GitHub Issue #76). Thanks for the bug report. Rustan

answered by: rustanleino wrote: Fixed (GitHub Issue #76). Thanks for the bug report. Rustan

inductive predicates

first post: jiplucap wrote: I guess that Dafny syntax doesn't allow to declare auxiliary variab...

filter_distributes_over_append

first post: jonnadal wrote: Dafny beginner here, and I'm struggling with what I assume is a sim...

latest post: jonnadal wrote: Had a flash of insight and came up with the following, but to be ho...

VS extension crashes

first post: TheodoreNorvell wrote: When I create a text file in Visual Studio and then rename it with ...

latest post: rustanleino wrote: I have not heard of this bug before. Can you please file it on http...

do-while loops

first post: TheodoreNorvell wrote: Is there a good way to deal with loops that will execute at least o...

latest post: rustanleino wrote: Just as in Java, you can use `break;` (without a label name) if you...

Dafny's result on VS, Rise4fun and CMD does not match

first post: AfsanehR wrote: I have ran into a problem. Some programs get verified when running ...

Can the verifier find a model even when the method is correct?

first post: TheodoreNorvell wrote: I was under the impression that when Z3 finds a model, it's a model...

latest post: TheodoreNorvell wrote: Good answers to this question can be found at Stack Exchange http:/...

answered by: TheodoreNorvell wrote: Good answers to this question can be found at Stack Exchange http:/...

Funciton calculating sum of modified array

first post: clynch wrote: I am trying to implement a greedy algorithm for load balancing. Th...

latest post: clynch wrote: Thank you for your quick and helpful answer. It makes sense. I ha...

Array to Sequence to Multisets and comparison

first post: AlexisChevalier wrote: Hello, I am a student working on my MSc dissertation and I use dafn...

latest post: AlexisChevalier wrote: Hello, I made some changes in my program this morning, I had not r...

answered by: AlexisChevalier wrote: Hello, I made some changes in my program this morning, I had not r...

asserting things about methods?

first post: rtmrtm wrote: I'd like to be able assert things about the results of Dafny method...

latest post: rustanleino wrote: The only way to do this is to add to both `m1` and `m2` some postco...