date:20181113

Re: [Why3-club] pb. with cloning

2018-11-13 Thread Andrei Paskevich

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 
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  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 
> 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
>> 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] pb. with cloning

2018-11-13 Thread 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  > 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 
> 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] pb. with cloning

2018-11-13 Thread Andrei Paskevich

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 
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
> 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

2018-11-13 Thread 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

Re: [Why3-club] pb. with cloning

Re: [Why3-club] pb. with cloning

[Why3-club] pb. with cloning

4 matches

Site Navigation

Mail list logo

Footer information