vladstejeroiu/dafny-programs

Examples of formal verifications written in Dafny.

dafny-programs's Issues

exists expression involved in a function def is not allowed to depend on allocated refs

Dafny-programs/Bundle-closure/ndfs_final.dfy

Lines 63 to 72 in c0dafac

	function KeyInvariant(G:set<Node>):bool
	reads G
	requires graph(G)
	{
	forall s :: s in Blue(G) && s.accepting ==>
	// TODO: How to fix this?
	// a quantifier involved in a function definition is not allowed to depend on
	// the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'p'
	!exists p :: |p| > 1 && Path(G,s,s,p)
	}

I'm currently in the process of writing something similar using dafny 4 and have this exact issue. Is there a way to solve it other than switching to dafny 3?
Thank you in advance if you ever read this :)