[Why3-club] Pb. with the matrix library

Hi, I don't understand the errors I've got when I write the following module. File maze.mlw, line 5, characters 2-26: Symbol set is already defined in the current scope module Maze use import int.Int use import bool.Bool use import matrix.Matrix as M use import matrix.Syntax type

[Why3-club] defining a type invariant

Hi, I would like to define a type invariant related to an array type. If I write for example : type myarray = array int invariant { forall i:int. 0 <=i< length self -> my_predicate self[i] } then I get the following error message: type aliases cannot have invariants. So, I changed

[Why3-club] trying to use FsetSum.sum

Hi, I’d like to use the sum function of the set.FsetSum theory: function sum <> (set 'a) ('a -> int) : int I have a function f : ‘a -> int. When I am defining function sum_set (s: set ‘a) : int = sum s f I got the following error message: This term

Re: [Why3-club] Why3-club Digest, Vol 87, Issue 13

> Le 13 mars 2018 à 12:00, why3-club-requ...@lists.gforge.inria.fr a écrit : > > Le 12/03/2018 à 16:23, Sandrine Blazy a écrit : > >> I have a function f : ‘a -> int. When I am defining >> function sum_set (s: set ‘a) : int = sum s f >> >> I got the fo

[Why3-club] proof of a test program

Hi, I am using Why3 0.87.3 to prove the following test program of the selection sort given in the gallery of verified programs (http://toccata.lri.fr/gallery/selection_sort.en.html ). let test1 () = let a = make 3 0 in a[0] <- 7;

Re: [Why3-club] pb. with cloning

a purely logical predicate. > You should declare "lecolor" as "let predicate" and instantiate using "val le > = lecolor". > > Hope it helps, > Andrei > > On 13 November 2018 at 14:04, Sandrine Blazy <mailto:sandrine.bl...@irisa

[Why3-club] pb. with cloning

Hello, I would like to reuse the insertion sort from the Why3 gallery. The following code was working in version 0.87, but it is not accepted anymore by version 1.1.0. What is wrong with my lecolor predicate ? Best, Sandrine module InsertionSort (* from Why3 gallery *) type elt val

Re: [Why3-club] pb. with cloning

ith >B -> True > | W -> not (e2 = B) > | R -> e2 = R > end > > clone InsertionSort with type elt = color, val le = lecolor > = > > What version do you currenly use? > > A. > > > On 13 November 2018 at 14:

Re: [Why3-club] Why3-club Digest, Vol 95, Issue 2

looks like you forgot the first parameter "a" of "p" in "result <-> p > i". When I add it, this is accepted (and proved) with the most recent > version of Why3. > > -- > Jean-Christophe > > On 11/9/18 6:20 PM, Sandrine Blazy wrote: >

[Why3-club] keyboard shortcut for provers

Hello, In my why3 IDE, there is no keyboard shortcut for my installed provers. Instead of a shortcut, I see « VoidSymbol » for each of my provers. Is there a way to define a shortcut for a given prover ? Best, Sandrine ___ Why3-club mailing list

[Why3-club] strange loops in the sequence library

Hello, in the library of sequences, several definitions use a while loop that is never executed. For instance, the function set <> (s:seq 'a) (i:int) (v:'a) : seq 'a starts with while false do variant { 0 }

[Why3-club] Problem installing why3 using opam

Hi, can anyone help with this installation failure? Thanks, Sandrine % opam install why3 The following actions will be performed: ∗ install why3 1.3.1 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><>  [why3.1.3.1] found in cache <><> Processing actions

Re: [Why3-club] Why3-club Digest, Vol 119, Issue 2

> Le 4 déc. 2020 à 12:00, why3-club-requ...@lists.gforge.inria.fr a écrit : > > > Le 03/12/2020 à 09:24, Sandrine Blazy a écrit : > >> My other question is about TryWhy3: which version of why3 does it use? > > I am updating it at the time of release. So, it sh

[Why3-club] provers triggered by proof strategies

Hello, I am using why3 version 1.3.3 and would like to add the Z3 and E provers to the list of installed provers, so that they are triggered by proof strategies 0, 1 and more. I tried several versions (among those listed in provers-detection-data.conf), including Z3 version 4.8.4 (that is