Commit e40a14af authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

new example: 2-state DFA

parent 0beead85
module DfaExample
(** regular expressions on alphabet {0,1} *)
type char = Zero | One
clone import regexp.Regexp with type char = char
(** mutable input stream *)
use import option.Option
type stream model { mutable state: list char }
val input: stream
val get () : option char writes {input}
ensures { match old input.state with
| Cons c l -> input.state = l /\ result = Some c
| Nil -> old input.state = input.state = Nil /\ result = None end }
(** 2-state DFA to recognize words ending with a 1, that is (0|1)*1
--------- 1 -------->
+- state 1 state 2-------+
| ^ <-------- 0 --------- ^ |
+-0--/ \----- 1 --+
*)
constant r1 : regexp = Concat (Star (Alt (Char Zero) (Char One))) (Char One)
constant r2 : regexp = Alt Epsilon r1
lemma nil_notin_r1: not (mem Nil r1)
lemma ends_with_one:
forall w: list char.
mem w r1 <-> exists w': list char. w = w' ++ Cons One Nil
lemma zero_w_in_r1: forall w: list char. mem w r1 <-> mem (Cons Zero w) r1
lemma one_w_in_r1: forall w: list char. mem w r2 <-> mem (Cons One w) r1
lemma zero_w_in_r2: forall w: list char. mem w r1 <-> mem (Cons Zero w) r2
lemma one_w_in_r2: forall w: list char. mem w r2 <-> mem (Cons One w) r2
let rec astate1 () : bool
ensures { result = True <-> input.state = Nil /\ mem (old input.state) r1 }
=
match get () with
| None -> False
| Some Zero -> astate1 ()
| Some One -> astate2 ()
end
with astate2 () : bool
ensures { result = True <-> input.state = Nil /\ mem (old input.state) r2 }
=
match get () with
| None -> True
| Some Zero -> astate1 ()
| Some One -> astate2 ()
end
end
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive option (a:Type) {a_WT:WhyType a} :=
| None : option a
| Some : a -> option a.
Axiom option_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (option a).
Existing Instance option_WhyType.
Implicit Arguments None [[a] [a_WT]].
Implicit Arguments Some [[a] [a_WT]].
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* Why3 assumption *)
Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
a)), (0%Z <= (length l))%Z.
Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
(* Why3 assumption *)
Inductive char :=
| Zero : char
| One : char .
Axiom char_WhyType : WhyType char.
Existing Instance char_WhyType.
(* Why3 assumption *)
Inductive regexp :=
| Empty : regexp
| Epsilon : regexp
| Char : char -> regexp
| Alt : regexp -> regexp -> regexp
| Concat : regexp -> regexp -> regexp
| Star : regexp -> regexp .
Axiom regexp_WhyType : WhyType regexp.
Existing Instance regexp_WhyType.
(* Why3 assumption *)
Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list
a)) {struct l1}: (list a) :=
match l1 with
| Nil => l2
| (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
end.
Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((infix_plpl l (Nil :(list a))) = l).
Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), ((length (infix_plpl l1
l2)) = ((length l1) + (length l2))%Z).
(* Why3 assumption *)
Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x
l2)).
Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
a)), (mem x l) -> exists l1:(list a), exists l2:(list a),
(l = (infix_plpl l1 (Cons x l2))).
(* Why3 assumption *)
Definition word := (list char).
(* Why3 assumption *)
Inductive mem1 : (list char) -> regexp -> Prop :=
| mem_eps : (mem1 (Nil :(list char)) Epsilon)
| mem_char : forall (c:char), (mem1 (Cons c (Nil :(list char))) (Char c))
| mem_altl : forall (w:(list char)) (r1:regexp) (r2:regexp), (mem1 w r1) ->
(mem1 w (Alt r1 r2))
| mem_altr : forall (w:(list char)) (r1:regexp) (r2:regexp), (mem1 w r2) ->
(mem1 w (Alt r1 r2))
| mem_concat : forall (w1:(list char)) (w2:(list char)) (r1:regexp)
(r2:regexp), (mem1 w1 r1) -> ((mem1 w2 r2) -> (mem1 (infix_plpl w1 w2)
(Concat r1 r2)))
| mems1 : forall (r:regexp), (mem1 (Nil :(list char)) (Star r))
| mems2 : forall (w1:(list char)) (w2:(list char)) (r:regexp), (mem1 w1
r) -> ((mem1 w2 (Star r)) -> (mem1 (infix_plpl w1 w2) (Star r))).
(* Why3 assumption *)
Inductive stream :=
| mk_stream : (list char) -> stream .
Axiom stream_WhyType : WhyType stream.
Existing Instance stream_WhyType.
(* Why3 assumption *)
Definition state(v:stream): (list char) :=
match v with
| (mk_stream x) => x
end.
(* Why3 goal *)
Theorem nil_notin_r1 : ~ (mem1 (Nil :(list char))
(Concat (Star (Alt (Char Zero) (Char One))) (Char One))).
red; intro.
inversion H.
inversion H4.
rewrite <- H5 in H0.
destruct w1;
simpl in H0;
discriminate H0.
Qed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="CVC3"
version="2.4.1"/>
<prover
id="2"
name="Coq"
version="8.3pl4"/>
<file
name="../dfa_example.mlw"
verified="false"
expanded="true">
<theory
name="DfaExample"
locfile="../dfa_example.mlw"
loclnum="2" loccnumb="7" loccnume="17"
verified="false"
expanded="true">
<goal
name="nil_notin_r1"
locfile="../dfa_example.mlw"
loclnum="34" loccnumb="8" loccnume="20"
sum="ba0ea9ca4fb3a71d8890dc19b32937d5"
proved="true"
expanded="false"
shape="amemaNilar1N">
<proof
prover="2"
timelimit="8"
memlimit="1000"
edited="dfa_example_DfaExample_nil_notin_r1_1.v"
obsolete="false"
archived="false">
<result status="valid" time="1.68"/>
</proof>
</goal>
<goal
name="ends_with_one"
locfile="../dfa_example.mlw"
loclnum="36" loccnumb="8" loccnume="21"
sum="5566cd69ae8ef446c881ff7869b8079f"
proved="false"
expanded="true"
shape="ainfix =V0ainfix ++V1aConsaOneaNilEqamemV0ar1F">
</goal>
<goal
name="zero_w_in_r1"
locfile="../dfa_example.mlw"
loclnum="40" loccnumb="8" loccnume="20"
sum="c5379a40ddcdf96a03953829fc80e368"
proved="false"
expanded="true"
shape="amemaConsaZeroV0ar1qamemV0ar1F">
</goal>
<goal
name="one_w_in_r1"
locfile="../dfa_example.mlw"
loclnum="41" loccnumb="8" loccnume="19"
sum="9b3694df82907053575ef5816f8f7d5f"
proved="false"
expanded="true"
shape="amemaConsaOneV0ar1qamemV0ar2F">
</goal>
<goal
name="zero_w_in_r2"
locfile="../dfa_example.mlw"
loclnum="43" loccnumb="8" loccnume="20"
sum="3cc829cb151131f597cb1990e0e950a4"
proved="false"
expanded="true"
shape="amemaConsaZeroV0ar2qamemV0ar1F">
</goal>
<goal
name="one_w_in_r2"
locfile="../dfa_example.mlw"
loclnum="44" loccnumb="8" loccnume="19"
sum="7cc931c0012ee6a36a62469815035f94"
proved="false"
expanded="true"
shape="amemaConsaOneV0ar2qamemV0ar2F">
</goal>
<goal
name="WP_parameter astate1"
locfile="../dfa_example.mlw"
loclnum="46" loccnumb="10" loccnume="17"
expl="VC for astate1"
sum="d7f10fbaf3327e6b9769a05c4fcbcc10"
proved="true"
expanded="false"
shape="CV2aNoneamemV0aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V1aNilNaSomeaZeroamemV0aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueIamemV1aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueFFaSomeaOneamemV0aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V5aNilqainfix =V6aTrueIamemV1aAltaEpsilonaConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V5aNilqainfix =V6aTrueFFICV0aConsVVainfix =V2aSomeV7Aainfix =V1V8aNilainfix =V2aNoneAainfix =V1aNilAainfix =V0V1FFF">
<label
name="expl:VC for astate1"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
<goal
name="WP_parameter astate1.1"
locfile="../dfa_example.mlw"
loclnum="46" loccnumb="10" loccnume="17"
expl="1. postcondition"
sum="b35261aff4ac9655ab1b9f13b5920ea8"
proved="true"
expanded="false"
shape="CV2aNoneamemV0aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V1aNilNaSomeaZerotaSomeaOnetICV0aConsVVainfix =V2aSomeV3Aainfix =V1V4aNilainfix =V2aNoneAainfix =V1aNilAainfix =V0V1FFF">
<label
name="expl:VC for astate1"/>
<proof
prover="1"
timelimit="20"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.09"/>
</proof>
</goal>
<goal
name="WP_parameter astate1.2"
locfile="../dfa_example.mlw"
loclnum="46" loccnumb="10" loccnume="17"
expl="2. postcondition"
sum="13367b914989f216d2ea2c013c13c859"
proved="true"
expanded="false"
shape="CV2aNonetaSomeaZeroamemV0aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueIamemV1aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueFFaSomeaOnetICV0aConsVVainfix =V2aSomeV5Aainfix =V1V6aNilainfix =V2aNoneAainfix =V1aNilAainfix =V0V1FFF">
<label
name="expl:VC for astate1"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
<goal
name="WP_parameter astate1.2.1"
locfile="../dfa_example.mlw"
loclnum="46" loccnumb="10" loccnume="17"
expl="1. postcondition"
sum="1fe1eb3176c9c151f54279e21d952bfe"
proved="true"
expanded="false"
shape="CV2aNonetaSomeaZeroainfix =V3aNilIainfix =V4aTrueIamemV1aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueFFaSomeaOnetICV0aConsVVainfix =V2aSomeV5Aainfix =V1V6aNilainfix =V2aNoneAainfix =V1aNilAainfix =V0V1FFF">
<label
name="expl:VC for astate1"/>
<proof
prover="0"
timelimit="20"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="WP_parameter astate1.2.2"
locfile="../dfa_example.mlw"
loclnum="46" loccnumb="10" loccnume="17"
expl="2. postcondition"
sum="1a33f7e714b75ff6e46ed4fb6316e55a"
proved="true"
expanded="false"
shape="CV2aNonetaSomeaZeroamemV0aConcataStaraAltaCharaZeroaCharaOneaCharaOneIainfix =V4aTrueIamemV1aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueFFaSomeaOnetICV0aConsVVainfix =V2aSomeV5Aainfix =V1V6aNilainfix =V2aNoneAainfix =V1aNilAainfix =V0V1FFF">
<label
name="expl:VC for astate1"/>
<proof
prover="0"
timelimit="8"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal
name="WP_parameter astate1.2.3"
locfile="../dfa_example.mlw"
loclnum="46" loccnumb="10" loccnume="17"
expl="3. postcondition"
sum="1ad3706f90cd5c2d9612ad792f5323f9"
proved="true"
expanded="false"
shape="CV2aNonetaSomeaZeroainfix =V4aTrueIamemV0aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilIamemV1aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueFFaSomeaOnetICV0aConsVVainfix =V2aSomeV5Aainfix =V1V6aNilainfix =V2aNoneAainfix =V1aNilAainfix =V0V1FFF">
<label
name="expl:VC for astate1"/>
<proof
prover="0"
timelimit="8"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter astate1.3"
locfile="../dfa_example.mlw"
loclnum="46" loccnumb="10" loccnume="17"
expl="3. postcondition"
sum="6bb80a59b73f4ae77ba5970cb20be7dc"
proved="true"
expanded="false"
shape="CV2aNonetaSomeaZerotaSomeaOneamemV0aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueIamemV1aAltaEpsilonaConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueFFICV0aConsVVainfix =V2aSomeV5Aainfix =V1V6aNilainfix =V2aNoneAainfix =V1aNilAainfix =V0V1FFF">
<label
name="expl:VC for astate1"/>
<proof
prover="0"
timelimit="8"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.38"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter astate2"
locfile="../dfa_example.mlw"
loclnum="55" loccnumb="7" loccnume="14"
expl="VC for astate2"
sum="9e914ab61e555c48469d32eaf807ae31"
proved="true"
expanded="false"
shape="CV2aNoneamemV0aAltaEpsilonaConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V1aNilaSomeaZeroamemV0aAltaEpsilonaConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueIamemV1aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueFFaSomeaOneamemV0aAltaEpsilonaConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V5aNilqainfix =V6aTrueIamemV1aAltaEpsilonaConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V5aNilqainfix =V6aTrueFFICV0aConsVVainfix =V2aSomeV7Aainfix =V1V8aNilainfix =V2aNoneAainfix =V1aNilAainfix =V0V1FFF">
<label
name="expl:VC for astate2"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
<goal
name="WP_parameter astate2.1"
locfile="../dfa_example.mlw"
loclnum="55" loccnumb="7" loccnume="14"
expl="1. postcondition"
sum="3a7bd9e70eda6d691f13571ffd8fa8aa"
proved="true"
expanded="false"
shape="CV2aNoneamemV0aAltaEpsilonaConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V1aNilaSomeaZerotaSomeaOnetICV0aConsVVainfix =V2aSomeV3Aainfix =V1V4aNilainfix =V2aNoneAainfix =V1aNilAainfix =V0V1FFF">
<label
name="expl:VC for astate2"/>
<proof
prover="1"
timelimit="8"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.09"/>
</proof>
</goal>
<goal
name="WP_parameter astate2.2"
locfile="../dfa_example.mlw"
loclnum="55" loccnumb="7" loccnume="14"
expl="2. postcondition"
sum="259f5cbeaec9f34726649e6bba41cb78"
proved="true"
expanded="false"
shape="CV2aNonetaSomeaZeroamemV0aAltaEpsilonaConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueIamemV1aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueFFaSomeaOnetICV0aConsVVainfix =V2aSomeV5Aainfix =V1V6aNilainfix =V2aNoneAainfix =V1aNilAainfix =V0V1FFF">
<label
name="expl:VC for astate2"/>
<proof
prover="1"
timelimit="8"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.09"/>
</proof>
</goal>
<goal
name="WP_parameter astate2.3"
locfile="../dfa_example.mlw"
loclnum="55" loccnumb="7" loccnume="14"
expl="3. postcondition"
sum="5b82ce1fd64ac980d92269e9328c77f4"
proved="true"
expanded="false"
shape="CV2aNonetaSomeaZerotaSomeaOneamemV0aAltaEpsilonaConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueIamemV1aAltaEpsilonaConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueFFICV0aConsVVainfix =V2aSomeV5Aainfix =V1V6aNilainfix =V2aNoneAainfix =V1aNilAainfix =V0V1FFF">
<label
name="expl:VC for astate2"/>
<proof
prover="0"
timelimit="8"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.37"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment