[Why3-club] Pb. with the matrix library

[Sandrine Blazy]

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 board = matrix int

 predicate won (b : board) (x : int) (y : int) = 
b [ (x,y) ] = 2 
end

When I remove the  use import matrix.Syntax line, I've got the following error.

File maze.mlw, line 9, characters 6-7:
Unbound symbol 'mixfix []'

What's wrong with my b[ (x,y) ] notation ?

Thanks for your help,

Sandrine
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club

[Why3-club] defining a type invariant

[Sandrine Blazy]

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 my definition to the following one :
type tmyarray = { myarray : array int }
invariant { forall i:int. 0 <= i < length self.myarray ->
  my_predicate (self.myarray[i]) }

This definition is ok, but the use of a record requires to construct and
destruct many of such records in my spec and my code. So, I am wondering
if there is a better way to define my type invariant.

Best,

Sandrine



signature.asc
Description: Message signed with OpenPGP
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] trying to use FsetSum.sum

[Sandrine Blazy]

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 has type set 'a, but is expected to have type set1 ‘xi

What’s wrong with s in this definition ?

Best,
Sandrine



signature.asc
Description: Message signed with OpenPGP
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

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

[Sandrine Blazy]

> 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 following error message:
>> This term has type set 'a, but is expected to have type set1 ‘xi
>> 
>> What’s wrong with s in this definition ?
> 
> Given the error message, I would say that the "set" type used in "sum"
> later got shadowed by another type with the same name.
> 
Thanks !
Indeed, I was importing too many modules.

Best,

Sandrine


signature.asc
Description: Message signed with OpenPGP
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] proof of a test program

[Sandrine Blazy]

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; a[1] <- 3; a[2] <- 1;
   selection_sort a;
   assert { a [0] = 1 };
   assert { a [1] = 3 };
   assert { a [2] = 7 };
   a

None of my provers (Alt-Ergo, cvc3, cvc4, Eprover, Z3) is able to prove any of 
these 3 assertions. However, if I choose the "get counter-example" option in 
the preference window, then cvc4 manages to prove this test program.

Does it mean that I should always choose this "get counter-example" option, 
even if I am not using this feature ?

Thanks,

Sandrine


signature.asc
Description: Message signed with OpenPGP
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] pb. with cloning

[Sandrine Blazy]

Thanks for your prompt answer.
Unfortunately, in the instantiation, Why3 complains that "val le = lecolor"  is 
a syntax error.

Sandrine

> Le 13 nov. 2018 à 14:08, Andrei Paskevich  a écrit :
> 
> Hi Sandrine,
> 
> you try to instantiate a "val predicate" with 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.fr>> wrote:
> 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 predicate le elt elt
> 
>   clone relations.TotalPreOrder with
> type t = elt, predicate rel = le, axiom .
>   clone export list.Sorted with
> type t = elt, predicate le  = le, goal Transitive.Trans
> 
>   use list.List
>   use list.Permut
> 
>   let rec insert (x: elt) (l: list elt) : list elt
> requires { sorted l }
> ensures  { sorted result }
> ensures  { permut (Cons x l) result }
> variant  { l }
>   = match l with
> | Nil -> Cons x Nil
> | Cons y r -> if le x y then Cons x l else Cons y (insert x r)
> end
> 
>   let rec insertion_sort (l: list elt) : list elt
> ensures { sorted result }
> ensures { permut l result }
> variant { l }
>   = match l with
> | Nil -> Nil
> | Cons x r -> insert x (insertion_sort r)
> end
> 
> end
> 
>  module M
>   use list.List
> 
> type color = B | W | R
> 
> val (=) (x y : color) : bool
> ensures { result <-> x=y}
> 
> predicate lecolor (e1 e2: color) =
> match e1 with
>B -> True
>  | W -> not (e2 = B)
>  | R -> e2 = R
> end
> 
> clone InsertionSort with type elt = color, predicate le  = lecolor
> 
> (*  Illegal instantiation for symbol le *)
> 
> (* … *)
> end 
> 
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr <mailto:Why3-club@lists.gforge.inria.fr>
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club 
> <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

[Why3-club] pb. with cloning

[Sandrine Blazy]

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 predicate le elt elt

  clone relations.TotalPreOrder with
type t = elt, predicate rel = le, axiom .
  clone export list.Sorted with
type t = elt, predicate le  = le, goal Transitive.Trans

  use list.List
  use list.Permut

  let rec insert (x: elt) (l: list elt) : list elt
requires { sorted l }
ensures  { sorted result }
ensures  { permut (Cons x l) result }
variant  { l }
  = match l with
| Nil -> Cons x Nil
| Cons y r -> if le x y then Cons x l else Cons y (insert x r)
end

  let rec insertion_sort (l: list elt) : list elt
ensures { sorted result }
ensures { permut l result }
variant { l }
  = match l with
| Nil -> Nil
| Cons x r -> insert x (insertion_sort r)
end

end

 module M
  use list.List

type color = B | W | R

val (=) (x y : color) : bool
ensures { result <-> x=y}

predicate lecolor (e1 e2: color) =
match e1 with
   B -> True
 | W -> not (e2 = B)
 | R -> e2 = R
end

clone InsertionSort with type elt = color, predicate le  = lecolor
  
(*  Illegal instantiation for symbol le *)

(* … *)
end 

___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Re: [Why3-club] pb. with cloning

[Sandrine Blazy]

Thanks for your help.
I have removed the « predicate » keyword and it works.

Sandrine

> Le 13 nov. 2018 à 18:25, Andrei Paskevich  a écrit :
> 
> Hmm, the following works for me in master:
> =
> let predicate lecolor (e1 e2: color) =
> match e1 with
>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:22, Sandrine Blazy  <mailto:sandrine.bl...@irisa.fr>> wrote:
> Thanks for your prompt answer.
> Unfortunately, in the instantiation, Why3 complains that "val le = lecolor"  
> is a syntax error.
> 
> Sandrine
> 
> 
>> Le 13 nov. 2018 à 14:08, Andrei Paskevich > <mailto:andrei.paskev...@lri.fr>> a écrit :
>> 
>> Hi Sandrine,
>> 
>> you try to instantiate a "val predicate" with 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.fr>> wrote:
>> 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 predicate le elt elt
>> 
>>   clone relations.TotalPreOrder with
>> type t = elt, predicate rel = le, axiom .
>>   clone export list.Sorted with
>> type t = elt, predicate le  = le, goal Transitive.Trans
>> 
>>   use list.List
>>   use list.Permut
>> 
>>   let rec insert (x: elt) (l: list elt) : list elt
>> requires { sorted l }
>> ensures  { sorted result }
>> ensures  { permut (Cons x l) result }
>> variant  { l }
>>   = match l with
>> | Nil -> Cons x Nil
>> | Cons y r -> if le x y then Cons x l else Cons y (insert x r)
>> end
>> 
>>   let rec insertion_sort (l: list elt) : list elt
>> ensures { sorted result }
>> ensures { permut l result }
>> variant { l }
>>   = match l with
>> | Nil -> Nil
>> | Cons x r -> insert x (insertion_sort r)
>> end
>> 
>> end
>> 
>>  module M
>>   use list.List
>> 
>> type color = B | W | R
>> 
>> val (=) (x y : color) : bool
>> ensures { result <-> x=y}
>> 
>> predicate lecolor (e1 e2: color) =
>> match e1 with
>>B -> True
>>  | W -> not (e2 = B)
>>  | R -> e2 = R
>> end
>> 
>> clone InsertionSort with type elt = color, predicate le  = lecolor
>> 
>> (*  Illegal instantiation for symbol le *)
>> 
>> (* … *)
>> end 
>> 
>> ___
>> Why3-club mailing list
>> Why3-club@lists.gforge.inria.fr <mailto:Why3-club@lists.gforge.inria.fr>
>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club 
>> <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

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

[Sandrine Blazy]

Sorry for the noise.
Here is the example that is not accepted by why3 anymore.
I don’t understand why a[i] is expected to have type int.

Best,

Sandrine

-

module Mt
  use int.Int
  use bool.Bool
  use array.Array

type cell = A | B | C

predicate p (a: array cell) (i:int) = (a[i] = A)

let f (a: array cell) (i: int) : bool
requires {  0 <= i < length a }
ensures { result <-> p a i }
=
a [i] = A
(* This expression has type Mt.cell, but is expected to have type int *)

end

> Le 10 nov. 2018 à 12:00, why3-club-requ...@lists.gforge.inria.fr a écrit :
> 
> It 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:
>> Hi, 
>> 
>> the following example worked fine using why3 version 0.87.3.
>> How should I write it so that it becomes accepted by why3 version 1.1.0 ?
>> 
>> module M
>>  use int.Int
>>  use bool.Bool
>>  use array.Array
>> 
>> predicate p (a: array int) (i:int) = (a[i]=0)
>> 
>> let f (a: array int) (i: int) : bool
>> requires { 0 <= i < length a }
>> ensures { result <-> p i}
>> =
>> a[i] = 0
>> 
>> end

___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] keyboard shortcut for provers

[Sandrine Blazy]

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@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] strange loops in the sequence library

[Sandrine Blazy]

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 } () done;
Are these loops mandatory ?

Sandrine___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] Problem installing why3 using opam

[Sandrine Blazy]

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 <><><><><><><><><><><><><><><><><><><><><><><><><><>   
[ERROR] The compilation of why3 failed at 
"/Users/blazy/.opam/opam-init/hooks/sandbox.sh build make -j15 all opt byte".

#=== ERROR while compiling why3.1.3.1 =#
# context 2.0.7 | macos/x86_64 | ocaml-system.4.09.0 | 
https://opam.ocaml.org#3b3a3c0d 
# path~/.opam/default/.opam-switch/build/why3.1.3.1
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j15 all opt byte
# exit-code   2
# env-file~/.opam/log/why3-97766-d2c37b.env
# output-file ~/.opam/log/why3-97766-d2c37b.out
### output ###
# src/server/server-unix.c:244:3: error: implicitly declaring library function 
'memcpy' with type 'void *(void *, const void *, unsigned long)' 
[-Werror,-Wimplicit-function-declaration]
# [...]
#   ^
# src/server/server-unix.c:244:3: note: include the header  or 
explicitly provide a declaration for 'memcpy'
# src/server/server-unix.c:356:37: error: implicitly declaring library function 
'strerror' with type 'char *(int)' [-Werror,-Wimplicit-function-declaration]
#   unix_argv[0],unix_argv[0],strerror(errno));
# ^
# src/server/server-unix.c:356:37: note: include the header  or 
explicitly provide a declaration for 'strerror'
# Ocamlopt src/util/mlmpfr_wrapper.ml
# 6 errors generated.
# Ocamlopt src/util/util.ml
# make: *** [src/server/server-unix.o] Error 1
# make: *** Waiting for unfinished jobs___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

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

[Sandrine Blazy]

> 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 should be 1.3.3.


Thanks!

I managed to solve my other issue: I used why3 config —detect-provers 
(instead of why3 config --add-prover …) to install all the provers. 
Now all provers are detected by the proof strategies.

Best,
Sandrine___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

[Why3-club] provers triggered by proof strategies

[Sandrine Blazy]

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 mentioned in 
the documentation for proof strategies). However, none of them is triggered by 
strategies 0 and 1. Which version of Z3 and E should I use?

My other question is about TryWhy3: which version of why3 does it use ?

Thanks,
Sandrine___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club