CODEWITHSUNDEEP
formal-verificationwhy3why3ml
Jay Kruer
Jay Kruer

Reputation: 33

Calling my own function in a predicate in Why3

With the latest version of Why3 (1.0.0), when I attempt to do something like the following:

 let add_one (n: int) : int = n+1
 predicate is_successor_of (n: int) (m: int) = m = add_one n

I get an error of the form: File "../something.why", line x, characters y-z: unbound symbol 'add_one'. Am I doing something wrong? Most examples I have seen of WhyML code in fact use only built-in/standard library functions, but do call other predicates defined in the same file. Is there no similar way to call functions I've defined in the same file when defining a predicate?

Upvotes: 0

Views: 637

Answers (1)

Jay Kruer
Jay Kruer

Reputation: 33

Marking the original add_one function definition as pure, with the function keyword, seems to do the trick. It makes sense, as side-effects should not be admissible in predicates.

Upvotes: 1

Related Questions