Hi Evgeny, "let" — definition of a program function (prototype, contract, and body) "val" — declaration of a program function (prototype and contract only)
"let function" — definition of a pure (side-effect-free) program function which can also be used in specifications as a logical function symbol "let predicate" — definition of a pure Boolean program function which can also be used in specifications as a logical predicate symbol "val function" — declaration of a pure (side-effect-free) program function which can also be used in specifications as a logical function symbol "val predicate" — declaration of a pure Boolean program function which can also be used in specifications as a logical predicate symbol "function" — definition or declaration of a logical function symbol which can also be used as a program function in ghost code "predicate" — definition or declaration of a logical predicate symbol which can also be used as a Boolean program function in ghost code "let lemma" — definition of a special pure program function which serves not as an actual code to execute but to prove the function's contract as a lemma: "for all values of parameters, the precondition implies the postcondition". This lemma is then added to the logical context and is made available to provers. If this "lemma-function" produces a result, the lemma is "for all values of parameters, the precondition implies the existence of a result that satisfies the postcondition". Lemma-functions are mostly used to prove some property by induction directly in Why3, without resorting to an external higher-order proof assistant. Program functions (defined with "let" or declared with "val") can additionally be marked "ghost" (meaning that they can only be used in the ghost code and never translated into executable code) or "partial" (meaning that their execution can produce observable effects unaccounted by their specification, and thus they cannot be used in the ghost code). Thank you for the bug report about Pinterp, we will look into that. Generally speaking, functions without definition (i.e. those declared with "val") will not be executed by "why3 execute". However, a handful of those functions, dealing with the basic data types and structures (e.g., integers and arrays) are "built-in" in the execution engine and will be executed. Hope this helps, Andrei On Sat, 6 Apr 2019 at 16:50, Евгений Макаров <emaka...@gmail.com> wrote: > Hello, > > I am somewhat lost at different types of functions in Why3. I > understand that there are pure logical functions and program > functions, but I am confused by different types of declarations. Here > are my questions. > > What is the difference between val and let? Is it true that val is > used for declaring functions without a body and let for defining > function with a body? Can they be used for pure and program functions? > > What do keywords function, predicate and lemma (?) mean in function > definitions/declarations? What is the difference between "function f", > "let function f" and "let f", and similarly for "val"? > > How can one find out which functions from the standard library have > implementation (can be executed) and which don't? For example, both > function add from Impset and ([]<-) from Array are declared as val. > Can I run them both using "why3 execute"? > > Also, executing functions from Fset, for example, add 3 empty, results > in the message "anomaly: File "src/mlw/pinterp.ml", line 204, > characters 12-18: Assertion failed". > > I apologize if these questions are basic. I spend a lot of time > reading and searching through different parts of the manual, but the > clear picture is still not there, and I feel it takes too much time to > research this on my own. Please direct me to the relevant parts of the > documentation if necessary. > > Evgeny > _______________________________________________ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club >
_______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
