New example: regexp membership using residuals

ROADMAP

@@ -114,6 +114,9 @@
 == New Features to announce ==
 
 * fixed compilation bug with lablgtk 2.18
+* new clause "diverges"
+* clauses "reads" and "writes" accept an empty set
+* improved support for Isabelle
 
 == Final preparation ==
 

bench/bench

@@ -150,6 +150,8 @@ execute examples/verifythis_PrefixSumRec.mlw PrefixSumRec.bench
 execute examples/vstte10_queens.mlw NQueens.test8
 # fails: "Cannot decide condition of if: (not ((~)((<<)((~)(0), 8)) = 0))"
 # examples/queens.mlw --exec  NQueensBits.test8
+# fails: "let" are cloned as "val"
+# examples/in_progress/residual.mlw --exec Test.test_astar
 echo ""
 
 echo "=== Checking drivers ==="

examples/in_progress/residual.mlw

+
+(** {1 Decision of regular expression membership} *)
+
+(** Decision algorithm based on residuals *)
+
+module Residuals
+
+  type char
+
+  clone export regexp.Regexp with type char = char
+
+  let rec accepts_epsilon (r:regexp) : bool
+    variant { r }
+    ensures { result <-> mem Nil r }
+  = match r with
+    | Empty -> false
+    | Epsilon -> true
+    | Char _ -> false
+    | Alt r1 r2 -> accepts_epsilon r1 || accepts_epsilon r2
+    | Concat r1 r2 -> accepts_epsilon r1 && accepts_epsilon r2
+    | Star _ -> true
+    end
+
+  let lemma inversion_mem_star (c:char) (w:word) (r:regexp)
+     ensures { 
+       forall w' r'. w' = Cons c w /\ r' = Star r ->
+       mem w' r' ->
+       exists w1 w2. w = w1 ++ w2 /\ mem (Cons c w1) r /\ mem w2 r' }
+  = ()
+
+  lemma inversion_mem_star2 :
+    forall c w r. mem (Cons c w) (Star r) ->
+       exists w1 w2. w = w1 ++ w2 /\ mem (Cons c w1) r /\ mem w2 (Star r)
+
+  (** [residual r c] denotes the set of words [w] such that [mem c.w r] *)
+  let rec residual (r:regexp) (c:char) : regexp
+    variant { r }
+    ensures { forall w. mem w result <-> mem (Cons c w) r }
+  = match r with
+    | Empty -> Empty
+    | Epsilon -> Empty
+    | Char c' -> if c = c' then Epsilon else Empty
+    | Alt r1 r2 -> Alt (residual r1 c) (residual r2 c)
+    | Concat r1 r2 ->
+       if accepts_epsilon r1 then
+          Alt (Concat (residual r1 c) r2) (residual r2 c)
+       else Concat (residual r1 c) r2
+    | Star r1 ->
+      Concat (residual r1 c) r
+    end
+
+  let rec decide_mem (w:word) (r:regexp) : bool
+    variant { w }
+    ensures { result <-> mem w r }
+  = match w with
+    | Nil -> accepts_epsilon r
+    | Cons c w' -> decide_mem w' (residual r c)
+    end
+
+
+end
+
+
+module Test
+
+  type char = int 
+
+  clone import Residuals with type char = char
+
+  constant a : char = 65
+
+  constant aa : word = Cons a (Cons a Nil)
+ 
+  constant astar : regexp = Star (Char a)
+
+  let test_astar () = decide_mem aa astar
+
+end
\ No newline at end of file

examples/in_progress/residual/residual_Residuals_WP_parameter_inversion_mem_star_1.v

+(* This file is generated by Why3's Coq 8.4 driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require list.List.
+Require list.Length.
+Require int.Int.
+Require list.Mem.
+Require list.Append.
+
+(* Why3 assumption *)
+Definition unit := unit.
+
+(* Why3 assumption *)
+Definition char := Z.
+
+(* Why3 assumption *)
+Inductive regexp :=
+  | Empty : regexp
+  | Epsilon : regexp
+  | Char : Z -> regexp
+  | Alt : regexp -> regexp -> regexp
+  | Concat : regexp -> regexp -> regexp
+  | Star : regexp -> regexp.
+Axiom regexp_WhyType : WhyType regexp.
+Existing Instance regexp_WhyType.
+
+(* Why3 assumption *)
+Definition word := (list Z).
+
+(* Why3 assumption *)
+Inductive mem : (list Z) -> regexp -> Prop :=
+  | mem_eps : (mem nil Epsilon)
+  | mem_char : forall (c:Z), (mem (cons c nil) (Char c))
+  | mem_altl : forall (w:(list Z)) (r1:regexp) (r2:regexp), (mem w r1) ->
+      (mem w (Alt r1 r2))
+  | mem_altr : forall (w:(list Z)) (r1:regexp) (r2:regexp), (mem w r2) ->
+      (mem w (Alt r1 r2))
+  | mem_concat : forall (w1:(list Z)) (w2:(list Z)) (r1:regexp) (r2:regexp),
+      (mem w1 r1) -> ((mem w2 r2) -> (mem (List.app w1 w2) (Concat r1 r2)))
+  | mems1 : forall (r:regexp), (mem nil (Star r))
+  | mems2 : forall (w1:(list Z)) (w2:(list Z)) (r:regexp), (mem w1 r) ->
+      ((mem w2 (Star r)) -> (mem (List.app w1 w2) (Star r))).
+
+(* Why3 goal *)
+Theorem WP_parameter_inversion_mem_star : forall (c:Z) (w:(list Z))
+  (r:regexp), forall (w':(list Z)) (r':regexp), ((w' = (cons c w)) /\
+  (r' = (Star r))) -> ((mem w' r') -> exists w1:(list Z), exists w2:(list Z),
+  (w = (List.app w1 w2)) /\ ((mem (cons c w1) r) /\ (mem w2 r'))).
+(* Why3 intros c w r w' r' (h1,h2) h3. *)
+intros c w r w' r' (h1,h2) h3.
+induction h3; try (discriminate h2).
+discriminate h1.
+injection h2; clear h2; intros; subst.
+
+destruct w1.
+
+now apply IHh3_2.
+
+simpl in h1.
+injection h1; clear h1; intros; subst.
+exists w1.
+exists w2.
+split; auto.
+
+
+Qed.
+

examples/in_progress/residual/residual_Residuals_WP_parameter_residual_1.v

+(* This file is generated by Why3's Coq 8.4 driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require list.List.
+Require list.Length.
+Require int.Int.
+Require list.Mem.
+Require list.Append.
+
+(* Why3 assumption *)
+Definition unit := unit.
+
+(* Why3 assumption *)
+Definition char := Z.
+
+(* Why3 assumption *)
+Inductive regexp :=
+  | Empty : regexp
+  | Epsilon : regexp
+  | Char : Z -> regexp
+  | Alt : regexp -> regexp -> regexp
+  | Concat : regexp -> regexp -> regexp
+  | Star : regexp -> regexp.
+Axiom regexp_WhyType : WhyType regexp.
+Existing Instance regexp_WhyType.
+
+(* Why3 assumption *)
+Definition word := (list Z).
+
+(* Why3 assumption *)
+Inductive mem : (list Z) -> regexp -> Prop :=
+  | mem_eps : (mem nil Epsilon)
+  | mem_char : forall (c:Z), (mem (cons c nil) (Char c))
+  | mem_altl : forall (w:(list Z)) (r1:regexp) (r2:regexp), (mem w r1) ->
+      (mem w (Alt r1 r2))
+  | mem_altr : forall (w:(list Z)) (r1:regexp) (r2:regexp), (mem w r2) ->
+      (mem w (Alt r1 r2))
+  | mem_concat : forall (w1:(list Z)) (w2:(list Z)) (r1:regexp) (r2:regexp),
+      (mem w1 r1) -> ((mem w2 r2) -> (mem (List.app w1 w2) (Concat r1 r2)))
+  | mems1 : forall (r:regexp), (mem nil (Star r))
+  | mems2 : forall (w1:(list Z)) (w2:(list Z)) (r:regexp), (mem w1 r) ->
+      ((mem w2 (Star r)) -> (mem (List.app w1 w2) (Star r))).
+
+Axiom inversion_mem_star : forall (c:Z) (w:(list Z)) (r:regexp),
+  forall (w':(list Z)) (r':regexp), ((w' = (cons c w)) /\ (r' = (Star r))) ->
+  ((mem w' r') -> exists w1:(list Z), exists w2:(list Z),
+  (w = (List.app w1 w2)) /\ ((mem (cons c w1) r) /\ (mem w2 r'))).
+
+Axiom inversion_mem_star2 : forall (c:Z) (w:(list Z)) (r:regexp), (mem
+  (cons c w) (Star r)) -> exists w1:(list Z), exists w2:(list Z),
+  (w = (List.app w1 w2)) /\ ((mem (cons c w1) r) /\ (mem w2 (Star r))).
+
+(* Why3 goal *)
+Theorem WP_parameter_residual : forall (r:regexp) (c:Z),
+  match r with
+  | Empty => True
+  | Epsilon => True
+  | (Char c') => True
+  | (Alt r1 r2) => True
+  | (Concat r1 r2) => forall (result:bool), ((result = true) <-> (mem nil
+      r1)) -> ((result = true) -> forall (o:regexp), (forall (w:(list Z)),
+      (mem w o) <-> (mem (cons c w) r2)) -> forall (o1:regexp),
+      (forall (w:(list Z)), (mem w o1) <-> (mem (cons c w) r1)) ->
+      forall (w:(list Z)), (mem w (Alt (Concat o1 r2) o)) <-> (mem (cons c w)
+      r))
+  | (Star r1) => True
+  end.
+(* Why3 intros r c. *)
+intros r c.
+destruct r; auto.
+intros.
+split; intros.
+
+inversion H3; subst; clear H3.
+inversion H6; subst; clear H6.
+rewrite List.app_comm_cons.
+constructor; auto.
+now apply H2.
+rewrite <- List.app_nil_l with (l:= (c::w)%list).
+constructor.
+tauto.
+now apply H1.
+
+inversion H3; subst; clear H3.
+destruct w1.
+apply mem_altr.
+rewrite H1.
+rewrite <- H4.
+now simpl.
+apply mem_altl.
+simpl in H4.
+injection H4; intros; subst; clear H4.
+constructor.
+now rewrite H2.
+auto.
+Qed.
+

examples/in_progress/residual/residual_Residuals_WP_parameter_residual_2.v

+(* This file is generated by Why3's Coq 8.4 driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require list.List.
+Require list.Length.
+Require int.Int.
+Require list.Mem.
+Require list.Append.
+
+(* Why3 assumption *)
+Definition unit := unit.
+
+(* Why3 assumption *)
+Definition char := Z.
+
+(* Why3 assumption *)
+Inductive regexp :=
+  | Empty : regexp
+  | Epsilon : regexp
+  | Char : Z -> regexp
+  | Alt : regexp -> regexp -> regexp
+  | Concat : regexp -> regexp -> regexp
+  | Star : regexp -> regexp.
+Axiom regexp_WhyType : WhyType regexp.
+Existing Instance regexp_WhyType.
+
+(* Why3 assumption *)
+Definition word := (list Z).
+
+(* Why3 assumption *)
+Inductive mem : (list Z) -> regexp -> Prop :=
+  | mem_eps : (mem nil Epsilon)
+  | mem_char : forall (c:Z), (mem (cons c nil) (Char c))
+  | mem_altl : forall (w:(list Z)) (r1:regexp) (r2:regexp), (mem w r1) ->
+      (mem w (Alt r1 r2))
+  | mem_altr : forall (w:(list Z)) (r1:regexp) (r2:regexp), (mem w r2) ->
+      (mem w (Alt r1 r2))
+  | mem_concat : forall (w1:(list Z)) (w2:(list Z)) (r1:regexp) (r2:regexp),
+      (mem w1 r1) -> ((mem w2 r2) -> (mem (List.app w1 w2) (Concat r1 r2)))
+  | mems1 : forall (r:regexp), (mem nil (Star r))
+  | mems2 : forall (w1:(list Z)) (w2:(list Z)) (r:regexp), (mem w1 r) ->
+      ((mem w2 (Star r)) -> (mem (List.app w1 w2) (Star r))).
+
+Axiom inversion_mem_star : forall (c:Z) (w:(list Z)) (r:regexp),
+  forall (w':(list Z)) (r':regexp), ((w' = (cons c w)) /\ (r' = (Star r))) ->
+  ((mem w' r') -> exists w1:(list Z), exists w2:(list Z),
+  (w = (List.app w1 w2)) /\ ((mem (cons c w1) r) /\ (mem w2 r'))).
+
+Axiom inversion_mem_star2 : forall (c:Z) (w:(list Z)) (r:regexp), (mem
+  (cons c w) (Star r)) -> exists w1:(list Z), exists w2:(list Z),
+  (w = (List.app w1 w2)) /\ ((mem (cons c w1) r) /\ (mem w2 (Star r))).
+
+(* Why3 goal *)
+Theorem WP_parameter_residual : forall (r:regexp) (c:Z),
+  match r with
+  | Empty => True
+  | Epsilon => True
+  | (Char c') => True
+  | (Alt r1 r2) => True
+  | (Concat r1 r2) => True
+  | (Star r1) => forall (o:regexp), (forall (w:(list Z)), (mem w o) <-> (mem
+      (cons c w) r1)) -> forall (w:(list Z)), (mem w (Concat o r)) <-> (mem
+      (cons c w) r)
+  end.
+(* Why3 intros r c. *)
+intros r c.
+destruct r; auto.
+intros.
+split; intros.
+
+inversion H0; subst; clear H0.
+rewrite List.app_comm_cons.
+constructor; auto.
+rewrite <- H; auto.
+
+destruct (inversion_mem_star2 _ _ _ H0) as (w1 & w2 & h1 & h2 & h3).
+subst w.
+constructor; auto.
+now rewrite H.
+
+Qed.
+

examples/in_progress/residual/residual_Residuals_WP_parameter_residual_3.v

+(* This file is generated by Why3's Coq 8.4 driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require list.List.
+Require list.Length.
+Require int.Int.
+Require list.Mem.
+Require list.Append.
+
+(* Why3 assumption *)
+Definition unit := unit.
+
+(* Why3 assumption *)
+Definition char := Z.
+
+(* Why3 assumption *)
+Inductive regexp :=
+  | Empty : regexp
+  | Epsilon : regexp
+  | Char : Z -> regexp
+  | Alt : regexp -> regexp -> regexp
+  | Concat : regexp -> regexp -> regexp
+  | Star : regexp -> regexp.
+Axiom regexp_WhyType : WhyType regexp.
+Existing Instance regexp_WhyType.
+
+(* Why3 assumption *)
+Definition word := (list Z).
+
+(* Why3 assumption *)
+Inductive mem : (list Z) -> regexp -> Prop :=
+  | mem_eps : (mem nil Epsilon)
+  | mem_char : forall (c:Z), (mem (cons c nil) (Char c))
+  | mem_altl : forall (w:(list Z)) (r1:regexp) (r2:regexp), (mem w r1) ->
+      (mem w (Alt r1 r2))
+  | mem_altr : forall (w:(list Z)) (r1:regexp) (r2:regexp), (mem w r2) ->
+      (mem w (Alt r1 r2))
+  | mem_concat : forall (w1:(list Z)) (w2:(list Z)) (r1:regexp) (r2:regexp),
+      (mem w1 r1) -> ((mem w2 r2) -> (mem (List.app w1 w2) (Concat r1 r2)))
+  | mems1 : forall (r:regexp), (mem nil (Star r))
+  | mems2 : forall (w1:(list Z)) (w2:(list Z)) (r:regexp), (mem w1 r) ->
+      ((mem w2 (Star r)) -> (mem (List.app w1 w2) (Star r))).
+
+Axiom inversion_mem_star : forall (c:Z) (w:(list Z)) (r:regexp),
+  forall (w':(list Z)) (r':regexp), ((w' = (cons c w)) /\ (r' = (Star r))) ->
+  ((mem w' r') -> exists w1:(list Z), exists w2:(list Z),
+  (w = (List.app w1 w2)) /\ ((mem (cons c w1) r) /\ (mem w2 r'))).
+
+Axiom inversion_mem_star2 : forall (c:Z) (w:(list Z)) (r:regexp), (mem
+  (cons c w) (Star r)) -> exists w1:(list Z), exists w2:(list Z),
+  (w = (List.app w1 w2)) /\ ((mem (cons c w1) r) /\ (mem w2 (Star r))).
+
+(* Why3 goal *)
+Theorem WP_parameter_residual : forall (r:regexp) (c:Z),
+  match r with
+  | Empty => True
+  | Epsilon => True
+  | (Char c') => True
+  | (Alt r1 r2) => True
+  | (Concat r1 r2) => forall (result:bool), ((result = true) <-> (mem nil
+      r1)) -> ((~ (result = true)) -> forall (o:regexp),
+      (forall (w:(list Z)), (mem w o) <-> (mem (cons c w) r1)) ->
+      forall (w:(list Z)), (mem w (Concat o r2)) <-> (mem (cons c w) r))
+  | (Star r1) => True
+  end.
+intros r c.
+destruct r; auto.
+intros.
+split; intros.
+
+inversion H2; subst; clear H2.
+rewrite List.app_comm_cons.
+constructor; auto.
+now rewrite <- H1.
+
+inversion H2; subst; clear H2.
+destruct w1.
+tauto.
+simpl in H3.
+injection H3; intros; subst; clear H3.
+constructor; auto.
+now rewrite H1.
+Qed.
+

modules/string.mlw

@@ -9,13 +9,6 @@ module Char
 
   type char model { code : int }
 
-  val chr (x:int) : char
-    requires { 0 <= x <= 255 }
-    ensures  { result = { code = x } }
-
-  val code (c:char) : int
-    ensures  { result = c.code /\ 0 <= c.code <= 255 }
-
   function uppercase char : char
   function lowercase char : char
 
@@ -35,8 +28,12 @@ module Char
     forall c:int. 0 <= c < 65 \/ 90 < c <= 127 ->
       lowercase { code = c } = { code = c }
 
-  val uppercase (c:char) : char ensures { result = uppercase c }
-  val lowercase (c:char) : char ensures { result = lowercase c }
+  val chr (x:int) : char
+    requires { 0 <= x <= 255 }
+    ensures  { result = { code = x } }
+
+  val code (c:char) : int
+    ensures  { result = c.code /\ 0 <= c.code <= 255 }
 
   (*** TODO
      - compare ?

src/whyml/mlw_interp.ml

@@ -914,7 +914,7 @@ and eval_app env s ls tl =
                           iter3 prs tl1
                       | None::prs, _::tl1 ->
                         iter3 prs tl1
-                      | _ -> assert false
+                      | _ -> Vapp(ls,tl)
                     in iter3 prs tl1
                   else iter2 rem2
               in iter2 csl