From 7faabb31b45a9a98ac618ab3728ff7b178bda596 Mon Sep 17 00:00:00 2001 From: Arthur Correnson Date: Fri, 3 Feb 2023 10:31:33 +0100 Subject: [PATCH] udpate the code --- html/WiSE.equalities.html | 65 - html/WiSE.implem.bugfinder.html | 426 ---- html/WiSE.implem.bugfinder_proof.html | 687 ------ html/WiSE.lang.imp.html | 741 ------ html/WiSE.lang.imprec.html | 520 ----- html/WiSE.relations.html | 158 -- html/WiSE.streams.html | 392 ---- html/WiSE.symbolic.solver.html | 325 --- html/WiSE.symbolic.symex.html | 592 ----- html/WiSE.utils.html | 104 - html/config.js | 72 - html/coqdoc.css | 197 -- html/coqdocjs.css | 249 -- html/coqdocjs.js | 189 -- html/extract.html | 46 - html/indexpage.html | 3052 ------------------------- html/toc.html | 143 -- src/implem/bugfinder_proof.v | 53 +- 18 files changed, 15 insertions(+), 7996 deletions(-) delete mode 100644 html/WiSE.equalities.html delete mode 100644 html/WiSE.implem.bugfinder.html delete mode 100644 html/WiSE.implem.bugfinder_proof.html delete mode 100644 html/WiSE.lang.imp.html delete mode 100644 html/WiSE.lang.imprec.html delete mode 100644 html/WiSE.relations.html delete mode 100644 html/WiSE.streams.html delete mode 100644 html/WiSE.symbolic.solver.html delete mode 100644 html/WiSE.symbolic.symex.html delete mode 100644 html/WiSE.utils.html delete mode 100644 html/config.js delete mode 100644 html/coqdoc.css delete mode 100644 html/coqdocjs.css delete mode 100644 html/coqdocjs.js delete mode 100644 html/extract.html delete mode 100644 html/indexpage.html delete mode 100644 html/toc.html diff --git a/html/WiSE.equalities.html b/html/WiSE.equalities.html deleted file mode 100644 index 6c9c2f2..0000000 --- a/html/WiSE.equalities.html +++ /dev/null @@ -1,65 +0,0 @@ - - - - - - - - - - - - - -
-
-

WiSE.equalities

- -
-
- -
-

Types With Equalities

- -
-
- -
-Class Eq (A : Type) := EQ {
-  eq_op : A -> A -> Prop;
-}.
- -
-Infix "≡" := eq_op (at level 80).
- -
-Definition bijection (A B : Type) `{Eq A} `{Eq B} (f : A -> B) (g : B -> A) :=
-  (forall a, g (f a) ≡ a) /\ (forall b, f (g b) ≡ b).
- -
-Definition isomorph (A B : Type) `{Eq A} `{Eq B} :=
-  exists f g, bijection A B f g.
- -
-Infix "≃" := isomorph (at level 80).
-
-
- -
- - - diff --git a/html/WiSE.implem.bugfinder.html b/html/WiSE.implem.bugfinder.html deleted file mode 100644 index 47380ac..0000000 --- a/html/WiSE.implem.bugfinder.html +++ /dev/null @@ -1,426 +0,0 @@ - - - - - - - - - - - - - -
-
-

WiSE.implem.bugfinder

- -
-From Coq Require Import List Lia String ZArith.
-From WiSE Require Import streams imp symbolic.symex.
-Import ListNotations.
- -
-
- -
-

Implementation of a naive bug finder for IMP

- -
- - A task list is a list of programs to be executed in a given symbolic state. -
-
-Definition tasks := list sym_state.
- -
-
- -
-A status corresponds to the current state of the bugfinding loop -
-
-Inductive status :=
-  | BugFound (s : sym_state)
-  | Pending
-  | Finished.
- -
-Definition then_do q '(((path, env), p) : sym_state) :=
-  ((path, env), Seq p q).
- -
-
- -
-Executing a task according to sym_step -
-
-Fixpoint expand path env prog : list sym_state :=
-  match prog with
-  | Skip => []
-  | Aff x e =>
-    [(path, sym_update env x (sym_aeval env e), Skip)]
-  | Err => []
-  | Ite b p1 p2 =>
-    [
-      (Band path (sym_beval env b), env, p1);
-      (Band path (Bnot (sym_beval env b)), env, p2)
-    ]
-  | Loop b p =>
-    [
-      (Band path (sym_beval env b), env, Seq p (Loop b p));
-      (Band path (Bnot (sym_beval env b)), env, Skip)
-    ]
-  | Seq Skip p2 => [(path, env, p2)]
-  | Seq p1 p2 =>
-    List.map (then_do p2) (expand path env p1)
-  end.
- -
-
- -
-Bugfinding loop: at every iteration, a task is choosen and then executed. - If the execution results in an error, a BugFound message is - emitted. If executing the task terminates in a state s without error, - a message Clear s is emitted. If executing the task generates a list l of subtasks, - then the loop signals that further computations are pending and add l to the worklist. - Finally, if the task list is empty, the loop emits the token Finished continuously. - -
-
-CoFixpoint run (l : tasks) : stream (option sym_state) :=
-  match l with
-  | [] => scons None (run [])
-  | ((path, env), prog)::next =>
-    let next_next := expand path env prog in
-    scons (Some (path, env, prog)) (run (next ++ next_next))
-  end.
- -
-
- -
-run_n predicts the tasks list after n iteration -
-
-Fixpoint run_n (n : nat) (tasks : list sym_state) : list sym_state :=
-  match n, tasks with
-  | 0, _ => tasks
-  | S n, [] => []
-  | S n, (path, env, prog)::next =>
-    let next_next := expand path env prog in
-    run_n n (next ++ next_next)
-  end.
- -
-Definition display (st : option sym_state) : status :=
-  match st with
-  | None => Finished
-  | Some (path, env, prog) =>
-    if is_error prog then BugFound (path, env, prog)
-    else Pending
-    (* else if is_skip prog then Clear (path, env, prog)
-    else Pending (path, env, prog) *)
-  end.
- -
-Definition init (p : IMP) : list sym_state :=
-  [((Bcst true, id), p)].
- -
-Definition find_bugs (p : IMP) : stream status :=
-  map display (run (init p)).
- -
-Definition init_assuming (p : IMP) (cond : bexpr) :=
-  [(cond, id, p)].
- -
-Definition find_bugs_assuming (p : IMP) (cond : bexpr) : stream status :=
-  map display (run (init_assuming p cond)).
- -
-
- -
-Examples -
-
-Section Examples.
- -
-Section Simple.
-Example my_prog :=
-  Ite
-    (Beq (Var "x"%string) (Cst 0%Z))
-    Err
-    Skip.
-Compute (peek 10 (find_bugs my_prog)).
-Example a := (Var "a"%string).
-Example b := (Var "b"%string).
-Example trivial_assertion :=
-  Seq
-    (Aff "a"%string b)
-    (Assert (Bnot (Beq a b))).
-Compute (peek 10 (find_bugs trivial_assertion)).
-End Simple.
- -
-Section Gcd.
- -
-(*
-function gcd(a, b)
-    while a ≠ b 
-        if a <= b
-            b := b − a
-        else
-            a := a − b
-    return a
-*)
- -
-Example gcd :=
-  Loop
-    (Bnot (Beq a b))
-    (Ite
-       (Ble a b)
-       (Aff "b"%string (Sub b a))
-       (Aff "a"%string (Sub a b))).
- -
-Example init_store (x : ident) : Z :=
-  match x with
-  | "a"%string => 9
-  | "b"%string => 6
-  | _ => 0
-  end.
- -
-(* gcd(9, 6) --> (3, 3) *)
-Example execute_gcd:
-  exec
-    init_store
-    gcd
-    (update (update init_store "a"%string 3%Z) "b"%string 3%Z).
-Proof.
-  unfold gcd.
- -
-  (* First Iteration *)
-  apply exec_loop_true with
-    (update init_store "a"%string 3%Z);
-  auto.
-  1: (* correctness of provided store *)
-  apply exec_Ite_false; auto.
-  apply exec_Aff.
-  auto.
- -
-  (* Second Iteration *)
-  apply exec_loop_true with
-    (update (update init_store "a"%string 3%Z) "b"%string 3%Z); auto.
- -
-  1: (* correctness of provided store *)
-  apply exec_Ite_true; auto.
-  apply exec_Aff.
-  auto.
- -
-  (* Termination *)
-  apply exec_loop_false.
-  auto.
-Qed.
- -
-Example a0 := (Var "a0"%string).
-Example b0 := (Var "b0"%string).
- -
-(* Now, a correct version of `gcd` with assertions. *)
- -
-(*
-function gcd(a, b)
-    while a ≠ b 
-        if a <= b
-            b := b − a
-        else
-            a := a − b
-        
-        assert a + b + 1 <= \old(a) + \old(b)
-    return a
-*)
- -
-Example gcd_assertions :=
-  Loop
-    (Bnot (Beq a b))
-    (Seq
-      (Aff "a0"%string a)
-      (Seq
-        (Aff "b0"%string b)
-        (Seq
-          (Ite
-             (Ble a b)
-             (Aff "b"%string (Sub b a))
-             (Aff "a"%string (Sub a b)))
-          (Assert (Ble (Add (Add a b) (Cst 1%Z)) (Add a0 b0)))))).
- -
-Example init_store' (x : ident) : Z :=
-  match x with
-  | "a"%string => 4
-  | "b"%string => 2
-  | _ => 0
-  end.
- -
-(* gcd(4, 2) --> (2, 2) *)
-Example execute_gcd_noerr:
-  exec
-    init_store'
-    gcd_assertions
-    (update
-      (update
-        (update init_store' "a0"%string 4)
-        "b0"%string 2)
-      "a"%string 2).
-  unfold gcd_assertions.
- -
-  (* First Iteration *)
-  apply exec_loop_true with
-    (update
-      (update
-        (update init_store' "a0"%string 4)
-        "b0"%string 2)
-      "a"%string 2);
-  auto.
- -
-  1: (* correctness of provided store *)
-  (* `a0 = a` *)
-  apply exec_Seq with (update init_store' "a0"%string 4%Z);
-  try constructor; auto.
- -
-  (* `b0 = b` *)
-  apply exec_Seq with
-    (update (update init_store' "a0"%string 4%Z) "b0"%string 2%Z);
-  try constructor; auto.
- -
-  (* if... ; ... *)
-  apply exec_Seq with
-    (update
-      (update
-        (update init_store' "a0"%string 4%Z)
-        "b0"%string 2%Z)
-      "a"%string 2%Z).
- -
-  1: (* if ... *)
-  apply exec_Ite_false; auto.
-  apply exec_Aff.
-  auto.
- -
-  (* assert ... *)
-  unfold Assert.
-  apply exec_Ite_true; auto.
-  apply exec_Skip.
- -
-  (* Termination *)
-  apply exec_loop_false.
-  auto.
-Qed.
- -
-(* Now, a *buggy* version of `gcd` with assertions. *)
- -
-(*
-function gcd_buggy(a, b)
-    while a ≠ b 
-        if a <= b
-            b := b − a
-        else
-            a := a + b  // Should be `a - b`
-        
-        assert a + b + 1 <= \old(a) + \old(b)
-    return a
-*)
- -
-Example gcd_buggy :=
-  Loop
-    (Bnot (Beq a b))
-    (Seq
-      (Aff "a0"%string a)
-      (Seq
-        (Aff "b0"%string b)
-        (Seq
-          (Ite
-             (Ble a b)
-             (Aff "b"%string (Sub b a))
-             (Aff "a"%string (Add a b)))
-          (Assert (Ble (Add (Add a b) (Cst 1%Z)) (Add a0 b0)))))).
- -
-(* gcd_buggy(4, 2) --> Err *)
-Example execute_gcd_err:
-  forall s, ~ exec init_store' gcd_buggy s.
-  intros s.
-  unfold not; intros.
-  inversion H; try (inversion H4; fail).
- -
-  inversion H4; clear H4 H2; subst; simpl in *.
-  inversion H12; clear H12; subst; simpl in *.
-  inversion H5; clear H5; subst; simpl in *.
-  inversion H4; clear H4; subst; simpl in *.
- -
-  - (* then case *)
-    inversion H3; clear H3; subst; simpl in *.
-    inversion H10; clear H10; subst; simpl in *.
-    inversion H9.
-  - (* else case *)
-    inversion H11; clear H11; subst; simpl in *.
-    inversion H3; clear H3; subst; simpl in *.
-    inversion H10; clear H10; subst; simpl in *.
-    inversion H8; clear H8; subst; simpl in *; inversion H5.
-    inversion H7.
-Qed.
-Notation "'Bug' π" := (BugFound (π, _, _)) (at level 80).
-Eval compute in (peek 20 (find_bugs gcd_buggy)).
-End Gcd.
- -
-End Examples.
-
-
- -
- - - diff --git a/html/WiSE.implem.bugfinder_proof.html b/html/WiSE.implem.bugfinder_proof.html deleted file mode 100644 index 038b8ea..0000000 --- a/html/WiSE.implem.bugfinder_proof.html +++ /dev/null @@ -1,687 +0,0 @@ - - - - - - - - - - - - - -
-
-

WiSE.implem.bugfinder_proof

- -
-From Coq Require Import List Lia String ZArith Program.Equality.
-From WiSE Require Import streams lang.imp symbolic.symex implem.bugfinder.
-Import ListNotations.
-Import LTL.
- -
-
- -
-

Correctness proof of the bugfinder

- -
- -

Soundness and Completness of expand w.r.t sym_step

- -
-
- -
-Lemma map_in:
-  forall A B (f : A -> B) (l : list A) b,
-    In b (List.map f l) -> exists a, In a l /\ b = f a.
-Proof.
-  intros. induction l; try easy.
-  destruct H as [<- | H].
-  - repeat econstructor.
-  - specialize (IHl H) as (a' & Ha' & ->).
-    exists a'. split; auto. now right.
-Qed.
- -
-
- -
-expand is a sound implementation of sym_step -
-
-Theorem expand_sound:
-  forall path env prog t,
-    In t (expand path env prog) -> sym_step ((path, env), prog) t.
-Proof.
-  intros path env prog [[path' env'] prog'] Hin.
-  induction prog in path', env', prog', Hin |-*; subst; try easy.
-  - destruct Hin as [[=<-<-<-] | [ [=<-<-<-] | [] ]]; constructor.
-  - destruct prog1; try easy.
-    + destruct Hin as [[=<-<-<-] | []]. now econstructor.
-    + pose proof (map_in _ _ _ _ _ Hin) as ([[path2 env2] prog3] & [H1 [=->->->]]).
-      specialize (IHprog1 _ _ _ H1).
-      now constructor.
-    + pose proof (map_in _ _ _ _ _ Hin) as ([[path2 env2] prog3] & [H1 [=->->->]]).
-      specialize (IHprog1 _ _ _ H1).
-      now constructor.
-    + pose proof (map_in _ _ _ _ _ Hin) as ([[path2 env2] prog3] & [H1 [=->->->]]).
-      specialize (IHprog1 _ _ _ H1).
-      now constructor.
-    + pose proof (map_in _ _ _ _ _ Hin) as ([[path2 env2] prog3] & [H1 [=->->->]]).
-      specialize (IHprog1 _ _ _ H1).
-      now constructor.
-  - destruct Hin as [[=<-<-<-] | []]. now constructor.
-  - destruct Hin as [[=<-<-<-] | [[=<-<-<-]| []]]; now constructor.
-Qed.
- -
-
- -
-expand is a complete implementation of sym_step -
-
-Theorem expand_complete:
-  forall path env prog t,
-    sym_step ((path, env), prog) t ->
-    In t (expand path env prog).
-Proof.
-  intros * Ht.
-  dependent induction Ht; intros; simpl.
-  - now econstructor.
-  - change (π2, s2, Seq c2 c3) with (then_do c3 (π2, s2, c2)).
-    destruct c1; try easy.
-    all: eapply in_map, IHHt; eauto.
-  - now left.
-  - now left.
-  - now (right; left).
-  - now left.
-  - now (right; left).
-Qed.
- -
-
- -
-expand spawns 0, 1 or 2 tasks -
-
-Theorem expand_inv:
-  forall path env prog,
-    (expand path env prog = []) \/
-    (exists s, expand path env prog = [s]) \/
-    (exists s1 s2, expand path env prog = [s1; s2]).
-Proof.
-  intros. induction prog.
-  - now left.
-  - now right; right; repeat econstructor.
-  - destruct IHprog1 as [IH | [(s & Hs) | (s1 & s2 & Hs)]].
-    + destruct prog1; simpl in *; try easy.
-      now right; left; repeat econstructor. rewrite IH.
-      now left.
-      now left.
-    + destruct prog1; simpl in *; try easy.
-      right. repeat econstructor. now rewrite Hs.
-      right. repeat econstructor.
-    + destruct prog1; simpl in *; try easy.
-      now right; right; repeat econstructor.
-      now right; right; repeat econstructor; rewrite Hs.
-      right; right; repeat econstructor; rewrite Hs.
-  - now right; left; repeat econstructor.
-  - now left.
-  - now right; right; repeat econstructor.
-Qed.
- -
-
- -
-

Eager model of run

- The run function that executes the main loop of the bugfinder - generates a lazy stream. Lazy streams are defined co-inductively - which make them somwhat hard to reason about. To ease the proofs, we - provide an eager implementation run_n of run that simulates the behavior of - run for n steps of computation. We then relate the 2 functions by a theorem run_run_n. - -
- - run_eq can be used to destruct applications of the cofixpoint run -
-
-Theorem run_eq:
-  forall l path env prog,
-    run ((path, env, prog)::l) = scons (Some (path, env, prog)) (run (l ++ expand path env prog)).
-Proof.
-  intros. now rewrite <- force_id at 1.
-Qed.
- -
-
- -
-the run [] is a fixpoint for shift i.e. - once the task list is empty, run loops indefinitely - in a state where the task list remains empty - -
-
-Lemma run_nil:
-  forall n, shift n (run []) = run [].
-Proof.
-  now induction n.
-Qed.
- -
-
- -
-Relation between run and its eager model run_n. - run_n n l computes the task list after n iterations run l - -
-
-Lemma run_run_n:
-  forall n l, shift n (run l) = run (run_n n l).
-Proof.
-  intros. induction n in l |-*; try easy.
-  destruct l as [| [[path env] prog] l] .
-  - apply run_nil.
-  - rewrite run_eq. simpl. now rewrite IHn.
-Qed.
- -
-Lemma run_n_nil:
-  forall n, run_n n [] = [].
-Proof.
-  now induction n.
-Qed.
- -
-
- -
-After List.length l1 iterations, the task list of run (l1 ++ l2) - starts with l2 - -
-
-Theorem run_n_length:
-  forall l1 l2,
-    exists l3,
-      run_n (List.length l1) (l1 ++ l2) = l2 ++ l3.
-Proof.
-  intros. induction l1 as [|[[path env] prog] l1 IH] in l2 |-*.
-  - simpl. exists []. now rewrite app_nil_r.
-  - simpl. rewrite <- List.app_assoc.
-    specialize (IH (l2 ++ expand path env prog)) as [l3 Hl3].
-    rewrite Hl3. rewrite <- List.app_assoc. now eexists.
-Qed.
- -
-
- -
-After 1 + List.length l1 iterations, the task list of run (t::l1 ++ l2) - starts with l2 followed with the task spawed by executing t - -
-
-Theorem run_n_S_length:
-  forall l1 l2 path env prog,
-    exists l3,
-      run_n (S (List.length l1)) ((path, env, prog)::l1 ++ l2) = l2 ++ (expand path env prog) ++ l3.
-Proof.
-  intros. induction l1 as [|[[path1 env1] prog1] l1 IH] in l2, path, env, prog |-*.
-  - simpl. exists []. now rewrite app_nil_r.
-  - simpl. do 2 rewrite <- List.app_assoc. simpl in IH.
-    specialize (IH (l2 ++ expand path env prog) path1 env1 prog1).
-    simpl in IH. edestruct IH as [l3 Hl3]. eexists.
-    repeat rewrite <- List.app_assoc in Hl3. apply Hl3.
-Qed.
- -
-
- -
-

LTL Specification Predicates

- - -
- - In the remainder of this file, we will use a shallow embedding of the LTL - logic to write specifications over lazy streams. - We start by defining some usefull LTL predicates. - -
- - The current state in the stream is sym_steps reachable from a state in l -
-
-Definition reachable_from (tasks : list sym_state) : LTL.t :=
-  now (fun s =>
-    match s with
-    | None => True
-    | Some s => exists s0, In s0 tasks /\ sym_steps s0 s
-    end
-  ).
- -
-
- -
-The current state in the stream is s -
-
-Definition here (s : sym_state) : LTL.t :=
-  now (fun st =>
-    match st with
-    | Some s' => s' = s
-    | None => False
-    end
-  ).
-Notation "! x" := (here x).
- -
-Definition bug_found s : LTL.t :=
-  now (fun (st : status) =>
-    match st with
-    | BugFound s' => s' = s
-    | _ => False
-    end
-  ).
-Notation "!! x" := (bug_found x).
- -
-Definition potential_bug p : LTL.t :=
-  now (fun (st : status) =>
-    match st with
-    | BugFound s' => potential_bug (Bcst true, id, p) s'
-    | _ => True
-    end
-  ).
- -
-Definition none : LTL.t :=
-  now (fun (st : option sym_state) =>
-    match st with
-    | None => True
-    | _ => False
-    end
-  ).
- -
-Definition done : LTL.t :=
-  now (fun (st : status) =>
-    match st with
-    | Finished => True
-    | _ => False
-    end
-  ).
- -
-
- -
-

Soundess of run

- -
- - run is sound with respect to sym_exec: - all states generate by the stream run l, - are reachable from l - -
-
-Theorem run_sound:
-  forall l,
-    run l ⊨ □ reachable_from l.
-Proof.
-  intros l n. rewrite run_run_n.
-  induction n in l |-*.
-  - simpl in *. destruct l as [| [[path env] prog]]; try easy.
-    repeat econstructor.
-  - destruct l as [| [[path env] prog] l]; try easy.
-    specialize (IHn (l ++ expand path env prog)).
-    simpl. destruct run_n as [| [[path1 env1] prog1]] eqn:Heq; try easy.
-    destruct IHn as [[[path2 env2] prog2] [[H | H]%in_app_iff Hsteps]].
-    + eexists. split; eauto. now right.
-    + pose proof (expand_sound _ _ _ _ H).
-      eexists. split. now left.
-      econstructor; eauto.
-Qed.
- -
-
- -
-

Completeness of run

- -
- - run is complete for sym_step: - if s is the next value generated by run l, then - all the direct sucessors of s are eventually generated - -
-
-Theorem run_step_complete:
-  forall l s s',
-    sym_step s s' ->
-    run l ⊨ (!s → ◊!s').
-Proof.
-  intros * Hstep H.
-  destruct l as [| [[path env] prog]]; try easy.
-  cbn in H. subst.
-  apply expand_complete in Hstep.
-  destruct (expand_inv path env prog) as [Htask | [[s Htask] | (s1 & s2 & Htask)]].
-  - now rewrite Htask in Hstep.
-  - rewrite run_eq, Htask in *. inversion Hstep; subst; try easy.
-    exists (S (List.length l)). simpl.
-    rewrite run_run_n.
-    pose proof (run_n_length l [s']) as [l3 Hl3].
-    replace (run_n (Datatypes.length l) (l ++ [s'])) with ([s'] ++ l3) at 1.
-    now destruct s' as [[a b] c].
-  - rewrite run_eq, Htask in *. destruct Hstep as [-> | [ -> | []]].
-    + exists (S (List.length l)). simpl.
-      rewrite run_run_n.
-      pose proof (run_n_length l [s'; s2]) as [l3 Hl3].
-      replace (run_n (Datatypes.length l) (l ++ [s'; s2])) with ([s'; s2] ++ l3) at 1.
-      simpl. now destruct s' as [[a b] c].
-    + exists (S (S (List.length l))). rewrite shift_eq.
-      rewrite run_run_n.
-      replace (l ++ [s1; s']) with ((l ++ [s1]) ++ [s']) at 1 by now rewrite <- List.app_assoc.
-      pose proof (run_n_length (l ++ [s1]) [s']) as [l3 Hl3].
-      replace (Datatypes.length (l ++ [s1])) with (S (Datatypes.length l)) in Hl3.
-      replace (run_n (S (Datatypes.length l)) ((l ++ [s1]) ++ [s'])) with ([s'] ++ l3) at 1.
-      now destruct s' as [[a b] c].
-      rewrite List.app_length. simpl. lia.
-Qed.
- -
-
- -
-run [s] immediately generates s -
-
-Theorem run_here:
-  forall s,
-    run [s] ⊨ here s.
-Proof.
-  now intros [[path env] prog].
-Qed.
- -
-
- -
-run is complete for sym_steps: - At any point in time, if s is generated by run l, then - all the sym_steps sucessors of s are eventually generated - -
-
-Theorem run_steps_complete:
-  forall s s',
-    sym_steps s s' ->
-    forall l,
-      run l ⊨ □ (!s → ◊!s').
-Proof.
-  intros s s' H.
-  dependent induction H.
-  - intros l n Hn. now exists 0.
-  - intros l n Hn. rewrite run_run_n in *.
-    pose proof (run_step_complete (run_n n l) _ _ H Hn) as [m Hm]. simpl in Hm.
-    specialize (IHstar _ _ Hm) as [k Hk].
-    rewrite shift_shift, run_run_n in Hk.
-    eexists (k + m). now rewrite run_run_n.
-Qed.
- -
-
- -
-run is a complete wau to compute the sym_steps sucessors - of any state s: - starting with the task [s], run [s] eventually generates - all sym_steps sucessors of s - -
-
-Theorem run_complete:
-  forall s s',
-    sym_steps s s' -> run [s] ⊨ ◊!s'.
-Proof.
-  intros.
-  now pose proof (run_steps_complete _ _ H [s] 0 (run_here s)).
-Qed.
- -
-Theorem run_finished_nil:
-  forall l,
-    none (run l) -> l = [].
-Proof.
-  now intros [|[[path env] prog]].
-Qed.
- -
-Theorem run_finished:
-  forall l,
-    run l ⊨ □ (none → □ none).
-Proof.
-  intros l n Hn m.
-  rewrite run_run_n in Hn.
-  apply run_finished_nil in Hn.
-  rewrite run_run_n, Hn.
-  now rewrite run_nil.
-Qed.
- -
-
- -
-fin_bugs is sound: - For any program p, find_bugs p - emits warnings ONLY if it found a bug in p - -
-
-Theorem find_bugs_sound:
-  forall p,
-    find_bugs p ⊨ □ (potential_bug p).
-Proof.
-  intros. unfold find_bugs.
-  pose proof (run_sound (init p)).
-  intros n. specialize (H n).
-  unfold potential_bug, reachable_from, now in *.
-  rewrite get_shift in *. simpl get in *.
-  rewrite get_map in *. destruct display eqn:Heq1; try easy.
-  destruct get as [[[path env] prog]|] eqn:Heq2; simpl in Heq1; try easy.
-  destruct (is_error prog) eqn:Heq3.
-  apply is_error_correct in Heq3. injection Heq1 as <-.
-  now destruct H as [[[path0 env0] prog0] [[[=->->->]|] H2]].
-  now destruct is_skip.
-Qed.
- -
-
- -
-fin_bugs is complete: - For any program p, if it has a bug, - find_bugs p will eventually find it - -
-
-Theorem find_bugs_complete:
-  forall p s',
-    symex.potential_bug (Bcst true, id, p) s' ->
-    find_bugs p ⊨ ◊ (bug_found s').
-Proof.
-  intros p [[path env] prog] [H1 H2].
-  pose proof (run_complete _ _ H1) as [n Hn].
-  exists n. unfold find_bugs, bug_found, here, now in *.
-  rewrite get_shift in *. simpl in *.
-  rewrite get_map. unfold init.
-  destruct get eqn:Heq1; subst; try easy.
-  unfold display.
-  destruct is_error eqn:Heq2; try easy.
-  destruct prog; try easy.
-  apply is_error_correct in H2.
-  now rewrite H2 in Heq2.
-Qed.
- -
-
- -
-A symbolic state denotes a valid bug in - p if all states in its concretization are bugs - -
-
-Definition ValidBug p σ' :=
-  forall σ, Concrete σ' σ -> imp.IsBug p σ.
- -
-
- -
-A status message is valid wrt prog p - if it is a BugFound message reporting a ValidBug - or any other kind of status message - -
-
-Definition ValidStatus p :=
-  now (fun st =>
-    match st with
-    | BugFound σ' => ValidBug p σ'
-    | _ => True
-    end
-  ).
- -
-Definition Symbolic σ :=
-  now (fun st =>
-    match st with
-    | BugFound σ' => Concrete σ' σ
-    | _ => False
-    end
-  ).
- -
-Theorem relative_completeness:
-  forall p σ,
-    imp.IsBug p σ -> find_bugs p ⊨ ◊ Symbolic σ.
-Proof.
-  intros * [(V0 & σ' & [Hsteps Hequiv])%Reach_complete H].
-  pose proof (run_complete _ _ Hsteps) as [n Hn].
-  exists n.
-  unfold find_bugs, Symbolic, bug_found, here, now in *.
-  rewrite get_shift in *. simpl in *.
-  rewrite get_map. unfold init, display.
-  destruct get as [[[π senv] p']|]; auto.
-  rewrite <- Hn in Hequiv. destruct σ as [V ?].
-  destruct (is_error p') eqn:Herr.
-  - now exists V0.
-  - destruct Hequiv as [_ [-> ->]].
-    apply is_error_Stuck in H.
-    now rewrite H in Herr.
-Qed.
- -
-Theorem relative_soundness:
-  forall p,
-    find_bugs p ⊨ □ ValidStatus p.
-Proof.
-  intros.
-  (* cleary a reformulation of find_bugs_sound *)
-Admitted.
- -
-
- -
-

Main Correctness Theorem !!!!

- -
- - THE MAIN RESULT: - find_bugs p is correct ! - This statement means 2 things: - (1) For any bug in the program p, the bug is eventually going - to be discovered - (2) If a 'bugy path' is discovered, then any concrete - instance of this path is a bug - -
-
-(* Theorem find_bugs_correct:
-  forall env0 prog0 env1 prog1,
-    imp.bug (env0, prog0) (env1, prog1) <->
-    exists path2 env2 prog2,
-      simpath (env0, prog0) (env1, prog1) (path2, env2, prog2) /\
-      (◊ (bug_found (path2, env2, prog2))) (find_bugs prog0).
-Proof.
-  intros. split.
-  + intros (path2 & env2 & prog2 & Hbug Hpath)*)
- -
-
- -
-"termination" of the bugfinding loop: - If at any point in time find_bugs p emits - a Finished token, then the exploration of p - terminated. We encode this property by - asserting that after the first Finished token, - the only message that the loop will ever send is Finished - (i.e. it cannot find new bugs afterward) - -
-
-Theorem sound_termination:
-  forall p,
-    find_bugs p ⊨ □ (done → □ done).
-Proof.
-  intros p. unfold find_bugs.
-  pose proof (run_finished (init p)).
-  intros n Hn m.
-  assert (Hnone : none (shift n (run (init p)))).
-  { unfold none, done, now in Hn |-*. rewrite get_shift in *.
-    simpl in *. rewrite get_map in Hn.
-    destruct get as [[[path env] prog]|] eqn:Heq1; try easy.
-    simpl in Hn. destruct is_error eqn:Heq2; try easy.
-  }
-  specialize (H n Hnone m). clear Hn Hnone.
-  rewrite shift_shift in *.
-  unfold done, none, now in *.
-  rewrite get_shift in *. simpl in *.
-  rewrite get_map. now destruct get eqn:Heq.
-Qed.
-
-
- -
- - - diff --git a/html/WiSE.lang.imp.html b/html/WiSE.lang.imp.html deleted file mode 100644 index 5ff43b5..0000000 --- a/html/WiSE.lang.imp.html +++ /dev/null @@ -1,741 +0,0 @@ - - - - - - - - - - - - - -
-
-

WiSE.lang.imp

- -
-From Coq Require Import ZArith String Bool Program.Equality.
-From WiSE Require Import relations.
- -
-
- -
-

IMP, A toy imperative programming language

- -
- -

Syntax

- -
-
- -
-Definition ident := string.
- -
-
- -
-Expressions -
-
-Inductive aexpr : Type :=
-  | Var : ident -> aexpr
-  | Cst : Z -> aexpr
-  | Add : aexpr -> aexpr -> aexpr
-  | Sub : aexpr -> aexpr -> aexpr.
- -
-Fixpoint aeq (a1: aexpr) (a2: aexpr) : bool :=
-  match a1, a2 with
-  | Var id1, Var id2 => String.eqb id1 id2
-  | Cst c1, Cst c2 => Z.eqb c1 c2
-  | Add a1 a2, Add a3 a4 | Sub a1 a2, Sub a3 a4
-      => andb (aeq a1 a3) (aeq a2 a4)
-  | _, _ => false
-  end.
- -
-Lemma aeq_spec:
-  forall a b, aeq a b = true <-> a = b.
-Proof.
-  induction a; intro b; split; intro H; destruct b; try easy; simpl in *.
-  - destruct (String.eqb_spec i i0).
-    + rewrite <- e; easy.
-    + destruct (diff_false_true); easy.
-  - injection H.
-    intro eq.
-    rewrite <- eq.
-    destruct (String.eqb_spec i i); auto.
-  - destruct (Z.eqb_eq z z0).
-    destruct (H0 H); easy.
-  - injection H; intros; rewrite <- H0; destruct (Z.eqb_eq z z); auto.
-  - destruct (andb_true_iff (aeq a1 b1) (aeq a2 b2)) as [H_to_prop _].
-    destruct (H_to_prop H) as [H_a1_beq_b1 H_a2_beq_b2].
-    destruct (IHa1 b1) as [H_a1_beq_b1_to_prop _].
-    destruct (H_a1_beq_b1_to_prop H_a1_beq_b1).
-    destruct (IHa2 b2) as [H_a2_beq_b2_to_prop _].
-    destruct (H_a2_beq_b2_to_prop H_a2_beq_b2).
-    reflexivity.
-  - destruct (andb_true_iff (aeq a1 b1) (aeq a2 b2)) as [_ H_goal_to_prop].
-    injection H; intros; subst.
-    destruct (IHa1 b1) as [_ H_b1_eq_b1_to_prop].
-    destruct (IHa2 b2) as [_ H_b2_eq_b2_to_prop].
-    auto.
-  - destruct (andb_true_iff (aeq a1 b1) (aeq a2 b2)) as [H_to_prop _].
-    destruct (H_to_prop H) as [H_a1_beq_b1 H_a2_beq_b2].
-    destruct (IHa1 b1) as [H_a1_beq_b1_to_prop _].
-    destruct (H_a1_beq_b1_to_prop H_a1_beq_b1).
-    destruct (IHa2 b2) as [H_a2_beq_b2_to_prop _].
-    destruct (H_a2_beq_b2_to_prop H_a2_beq_b2).
-    reflexivity.
-  - destruct (andb_true_iff (aeq a1 b1) (aeq a2 b2)) as [_ H_goal_to_prop].
-    injection H; intros; subst.
-    destruct (IHa1 b1) as [_ H_b1_eq_b1_to_prop].
-    destruct (IHa2 b2) as [_ H_b2_eq_b2_to_prop].
-    auto.
-Qed.
- -
-Inductive bexpr : Type :=
-  | Bcst : bool -> bexpr
-  | Ble : aexpr -> aexpr -> bexpr
-  | Beq : aexpr -> aexpr -> bexpr
-  | Bnot : bexpr -> bexpr
-  | Band : bexpr -> bexpr -> bexpr.
- -
-Definition Bor (b1 b2 : bexpr) := Bnot (Band (Bnot b1) (Bnot b2)).
- -
-Fixpoint beq (b1: bexpr) (b2: bexpr) : bool :=
-  match b1, b2 with
-  | Bcst b1, Bcst b2 => eqb b1 b2
-  | Ble a1 a2, Ble a3 a4 | Beq a1 a2, Beq a3 a4
-      => andb (aeq a1 a3) (aeq a2 a4)
-  | Bnot b1, Bnot b2 => beq b1 b2
-  | Band b1 b2, Band b3 b4 => andb (beq b1 b3) (beq b2 b4)
-  | _, _ => false
-  end.
- -
-Lemma beq_spec:
-  forall a b, beq a b = true <-> a = b.
-Proof.
-  induction a; intro b0; split; intro H;
-  destruct b0; auto;
-  try (simpl in H; destruct (diff_false_true); easy).
-  - simpl in *;
-    destruct (eqb_spec b b0); inversion H; subst; auto.
-  - injection H; intro H_b_eq_b0; subst.
-    unfold beq.
-    destruct (eqb_spec b0 b0); easy.
-  - unfold beq in H.
-    destruct (andb_true_iff (aeq a a1) (aeq a0 a2)) as [H0 _].
-    destruct (H0 H) as [H1 H2].
-    destruct (aeq_spec a a1) as [H3 _].
-    destruct (aeq_spec a0 a2) as [H4 _].
-    destruct (H3 H1).
-    destruct (H4 H2).
-    easy.
-  - unfold beq.
-    apply (andb_true_iff (aeq a a1) (aeq a0 a2)).
-    inversion H; subst.
-    split; apply aeq_spec; reflexivity.
-  - unfold beq in H.
-    destruct (andb_true_iff (aeq a a1) (aeq a0 a2)) as [H0 _].
-    destruct (H0 H) as [H1 H2].
-    destruct (aeq_spec a a1) as [H3 _].
-    destruct (aeq_spec a0 a2) as [H4 _].
-    destruct (H3 H1).
-    destruct (H4 H2).
-    easy.
-  - unfold beq.
-    apply (andb_true_iff (aeq a a1) (aeq a0 a2)).
-    inversion H; subst.
-    split; apply aeq_spec; reflexivity.
-  - destruct (IHa b0) as [H_beq_a_b0_to_prop _].
-    simpl in *.
-    destruct (H_beq_a_b0_to_prop H).
-    reflexivity.
-  - injection H; intros H_a_eq_b0; subst.
-    simpl.
-    destruct (IHa b0) as [_ H0].
-    auto.
-  - simpl in *.
-    destruct (andb_true_iff (beq a1 b0_1) (beq a2 b0_2)) as [H0 _].
-    destruct (H0 H) as [H1 H2].
-    destruct (IHa1 b0_1) as [H3 _].
-    destruct (IHa2 b0_2) as [H4 _].
-    destruct (H3 H1).
-    destruct (H4 H2).
-    reflexivity.
-  - injection H; intros H1 H2; subst.
-    simpl in *.
-    destruct (IHa1 b0_1) as [_ H0].
-    destruct (IHa2 b0_2) as [_ H1].
-    destruct (andb_true_iff (beq b0_1 b0_1) (beq b0_2 b0_2)) as [_ H2].
-    auto.
-Qed.
- -
-
- -
-Commands -
-
-Inductive IMP : Type :=
-  | : IMP
-  | Ite : bexpr -> IMP -> IMP -> IMP
-  | Seq : IMP -> IMP -> IMP
-  | Aff : string -> aexpr -> IMP
-  | Err : IMP
-  | Loop : bexpr -> IMP -> IMP
-  .
- -
-Definition Assert c := Ite c Skip Err.
- -
-
- -
-

Semantics

- -
-
- -
-Definition store := ident -> Z.
- -
-
- -
-

Denotational semantics for expressions

- -
- - Semantic of Arithmetic expressions -
-
-Fixpoint aeval (s : store) (e : aexpr) : Z :=
-  match e with
-  | Var x => s x
-  | Cst c => c
-  | Add e1 e2 => aeval s e1 + aeval s e2
-  | Sub e1 e2 => aeval s e1 - aeval s e2
-  end.
- -
-Fixpoint asubst (e : aexpr) (x : ident) (e' : aexpr) :=
-  match e with
-  | Var y => if (y =? x)%string then e' else e
-  | Cst _ => e
-  | Add e1 e2 => Add (asubst e1 x e') (asubst e2 x e')
-  | Sub e1 e2 => Sub (asubst e1 x e') (asubst e2 x e')
-  end.
- -
-Definition ainst (e : aexpr) (x : ident) (vx : Z) :=
-  asubst e x (Cst vx).
- -
-Fixpoint beval (s : store) (e : bexpr) : bool :=
-  match e with
-  | Bcst b => b
-  | Ble e1 e2 => (aeval s e1 <=? aeval s e2)%Z
-  | Beq e1 e2 => (aeval s e1 =? aeval s e2)%Z
-  | Band e1 e2 => beval s e1 && beval s e2
-  | Bnot e => negb (beval s e)
-  end.
- -
-Fixpoint bsubst (e : bexpr) (x : ident) (e' : aexpr) :=
-  match e with
-  | Bcst _ => e
-  | Beq e1 e2 => Beq (asubst e1 x e') (asubst e2 x e')
-  | Ble e1 e2 => Ble (asubst e1 x e') (asubst e2 x e')
-  | Band e1 e2 => Band (bsubst e1 x e') (bsubst e2 x e')
-  | Bnot e => Bnot (bsubst e x e')
-  end.
- -
-Definition binst (e : bexpr) (x : ident) (vx : Z) :=
-  bsubst e x (Cst vx).
- -
-
- -
-

Operational semantics of IMP

- -
- - Updating a store -
-
-Definition update (s : store) (x : ident) (v : Z) : store :=
-  fun y => if (y =? x)%string then v else s y.
- -
-
- -
-Subtitution lemma (for arithmetic expressions) -
-
-Lemma aeval_asubst :
-  forall s e x e',
-    aeval s (asubst e x e') = aeval (update s x (aeval s e')) e.
-Proof.
-  induction e; intros; simpl in *; auto.
-  - unfold update.
-    destruct (String.eqb_spec i x); auto.
-  - now rewrite IHe1, IHe2.
-  - now rewrite IHe1, IHe2.
-Qed.
- -
-
- -
-Subtitution lemma (for boolean expressions) -
-
-Lemma beval_bsubst :
-  forall s c x e,
-    beval s (bsubst c x e) = beval (update s x (aeval s e)) c.
-Proof.
-  intros. induction c; simpl in *; auto.
-  all: try now do 2 rewrite <- aeval_asubst.
-  now rewrite IHc.
-  now rewrite IHc1, IHc2.
-Qed.
- -
-Lemma aeval_inst:
-  forall s e x vx, aeval (update s x vx) e = aeval s (ainst e x vx).
-Proof.
-  intros. unfold ainst.
-  now rewrite aeval_asubst.
-Qed.
- -
-Lemma beval_inst:
-  forall s c x vx, beval (update s x vx) c = beval s (binst c x vx).
-Proof.
-  intros. induction c; simpl; auto.
-  all: try now do 2 rewrite aeval_inst.
-  now rewrite IHc.
-  now rewrite IHc1, IHc2.
-Qed.
- -
-
- -
-Big step semantics -
-
-Inductive exec : store -> IMP -> store -> Prop :=
-  | exec_Skip s :
-    exec s Skip s
-  | exec_Aff s x e ve :
-    aeval s e = ve ->
-    exec s (Aff x e) (update s x ve)
-  | exec_Seq s s' s'' c1 c2 :
-    exec s c1 s' ->
-    exec s' c2 s'' ->
-    exec s (Seq c1 c2) s''
-  | exec_Ite_true s s' e c1 c2 :
-    beval s e = true ->
-    exec s c1 s' ->
-    exec s (Ite e c1 c2) s'
-  | exec_Ite_false s s' e c1 c2 :
-    beval s e = false ->
-    exec s c2 s' ->
-    exec s (Ite e c1 c2) s'
-  | exec_loop_true s s' s'' e c :
-    beval s e = true ->
-    exec s c s' ->
-    exec s' (Loop e c) s'' ->
-    exec s (Loop e c) s''
-  | exec_loop_false s e c :
-    beval s e = false ->
-    exec s (Loop e c) s.
- -
-
- -
-Small step semantics -
-
-Inductive step : (store * IMP) -> (store * IMP) -> Prop :=
-  | step_Aff s x e ve :
-    aeval s e = ve -> step (s, Aff x e) (update s x ve, Skip)
-  | step_Seq s1 s2 c1 c2 c3 :
-    step (s1, c1) (s2, c2) -> step (s1, Seq c1 c3) (s2, Seq c2 c3)
-  | step_Seq_Skip s c :
-    step (s, Seq Skip c) (s, c)
-  | step_Ite_true s e c1 c2 :
-    beval s e = true -> step (s, Ite e c1 c2) (s, c1)
-  | step_Ite_false s e c1 c2 :
-    beval s e = false -> step (s, Ite e c1 c2) (s, c2)
-  | step_Loop_true s e c :
-    beval s e = true -> step (s, Loop e c) (s, Seq c (Loop e c))
-  | step_Loop_false s e c :
-    beval s e = false -> step (s, Loop e c) (s, Skip).
- -
-Lemma aeval_stable:
-  forall env1 env2 e,
-    (forall x, env1 x = env2 x) ->
-    aeval env1 e = aeval env2 e.
-Proof.
-  intros.
-  induction e; simpl; auto.
-  - now rewrite IHe1, IHe2.
-  - now rewrite IHe1, IHe2.
-Qed.
- -
-
- -
-Sequences of steps -
-
-Definition steps := star step.
- -
-
- -
-Taking several steps to the left of a sequence -
-
-Lemma steps_seq :
-  forall s1 s2 c1 c2 c3,
-    steps (s1, c1) (s2, c2) -> steps (s1, Seq c1 c3) (s2, Seq c2 c3).
-Proof.
-  intros * H. dependent induction H.
-  * reflexivity.
-  * destruct y as [s1' c1'].
-    eapply star_step. apply step_Seq, H.
-    now apply IHstar.
-Qed.
- -
-
- -
- If a program p starting in state s terminates in - state s' then p can take a sequence of steps - from s to s' - -
-
-Theorem exec_steps :
-  forall p s s', exec s p s' -> steps (s, p) (s', Skip).
-Proof.
-  induction 1.
-  - reflexivity.
-  - eapply star_step.
-    + apply (step_Aff _ _ _ _ H).
-    + reflexivity.
-  - etransitivity. apply steps_seq, IHexec1.
-    eapply star_step. apply step_Seq_Skip.
-    apply IHexec2.
-  - eapply star_step. eapply (step_Ite_true _ _ _ _ H).
-    apply IHexec.
-  - eapply star_step. eapply (step_Ite_false _ _ _ _ H).
-    apply IHexec.
-  - eapply star_step. eapply (step_Loop_true _ _ _ H).
-    etransitivity. eapply (steps_seq _ _ _ _ _ IHexec1).
-    eapply star_step. eapply step_Seq_Skip. apply IHexec2.
-  - eapply star_step. eapply (step_Loop_false _ _ _ H).
-    reflexivity.
-Qed.
- -
-Theorem step_exec_exec :
-  forall c1 c2 s1 s2 s3,
-    step (s1, c1) (s2, c2) ->
-    exec s2 c2 s3 ->
-    exec s1 c1 s3.
-Proof.
-  intros * H1. generalize s3. clear s3.
-  dependent induction H1; intros.
-  - inversion_clear H.
-    now apply exec_Aff.
-  - inversion_clear H.
-    eapply exec_Seq; eauto.
-  - eapply exec_Seq; eauto using exec.
-  - eapply exec_Ite_true; eauto.
-  - eapply exec_Ite_false; eauto.
-  - inversion_clear H0.
-    eapply exec_loop_true; eauto.
-  - inversion H0; subst.
-    eapply exec_loop_false; eauto.
-Qed.
- -
-
- -
- If a program p can take a sequence of steps - from s to s' then p terminates in - state s' when executed in s - -
-
-Theorem steps_exec :
-  forall p s s', steps (s, p) (s', Skip) -> exec s p s'.
-Proof.
-  intros. dependent induction H.
-  - apply exec_Skip.
-  - destruct y as [s1 p1].
-    eapply step_exec_exec; eauto.
-Qed.
- -
-
- -
-

Progression and Erroneous States

- -
- - A configuration is said to progress if it is a Skip statement or - if it can take a step - -
-
-Definition progress '((s, p) : (store * IMP)) : Prop :=
-  p = Skip \/ exists s' p', step (s, p) (s', p').
- -
-
- -
-An error state is a state that can't progress -
-
-Definition error_state (st : (store * IMP)) : Prop :=
-  ~progress st.
- -
-
- -
-Skip can progress -
-
-Theorem progress_Skip:
-  forall env, progress (env, Skip).
-Proof.
-  now left.
-Qed.
- -
-
- -
-Ite can progress -
-
-Theorem progress_Ite:
-  forall env b p1 p2, progress (env, Ite b p1 p2).
-Proof.
-  intros *. right.
-  destruct (beval env b) eqn:Hsat.
-  * exists env, p1. now econstructor.
-  * exists env, p2. now econstructor.
-Qed.
- -
-
- -
-Aff can progress -
-
-Theorem progress_Aff:
-  forall env x e, progress (env, Aff x e).
-Proof.
-  intros *. right.
-  repeat econstructor.
-Qed.
- -
-
- -
-Aff can progress -
-
-Theorem progress_Seq:
-  forall env p1 p2, progress (env, p1) -> progress (env, Seq p1 p2).
-Proof.
-  intros * [-> | (s' & p' & H)].
-  - right. exists env, p2. econstructor.
-  - right. exists s', (Seq p' p2). now econstructor.
-Qed.
- -
-
- -
-Loop can progress -
-
-Theorem progress_Loop:
-  forall env b p, progress (env, Loop b p).
-Proof.
-  intros *. right.
-  destruct (beval env b) eqn:Hsat.
-  - exists env. now repeat econstructor.
-  - exists env, Skip. now repeat econstructor.
-Qed.
- -
-
- -
-If a sequence Seq p1 p2 can't progress, then p1 can't progress -
-
-Theorem error_state_seq:
-  forall s p1 p2, error_state (s, Seq p1 p2) -> error_state (s, p1).
-Proof.
-  intros * H Hcontr.
-  apply H, progress_Seq, Hcontr.
-Qed.
- -
-
- -
-Syntactic characterization of error states -
-
-Inductive error : IMP -> Prop :=
-  | error_Err : error Err
-  | error_Seq p1 p2 : error p1 -> error (Seq p1 p2).
- -
-Theorem error_state_error :
-  forall s p, error_state (s, p) <-> error p.
-Proof.
-  intros. split.
-  - intros Hcontr.
-    induction p; try easy.
-    + now specialize (Hcontr (progress_Skip s)).
-    + now specialize (Hcontr (progress_Ite s _ _ _)).
-    + apply error_state_seq in Hcontr.
-      specialize (IHp1 Hcontr). now econstructor.
-    + now specialize (Hcontr (progress_Aff s _ _)).
-    + econstructor.
-    + now specialize (Hcontr (progress_Loop s _ _)).
-  - induction 1.
-    + intros [H | (s' & p' & H)]; try easy.
-    + intros [H' | (s' & p' & H')]; try easy.
-      inversion H'; subst.
-      assert (Hprog : progress (s, p1)) by (right; repeat econstructor; eauto).
-      apply (IHerror Hprog).
-      inversion H.
-Qed.
- -
-
- -
-Executable check for erroneous state -
-
-Fixpoint is_error (p : IMP) : bool :=
-  match p with
-  | Err => true
-  | Seq p _ => is_error p
-  | _ => false
-  end.
- -
-Theorem is_error_correct:
-  forall p, is_error p = true <-> error p.
-Proof.
-  induction p; try easy.
-  - split.
-    + intros H%IHp1. now econstructor.
-    + intros. inversion H; subst.
-      simpl. now apply IHp1.
-  - repeat econstructor.
-Qed.
- -
-Definition is_skip (p : IMP) : bool :=
-  match p with
-  | Skip => true
-  | _ => false
-  end.
- -
-Definition bug (s s' : store * IMP) : Prop :=
-  let '(_, prog) := s' in
-  steps s s' /\ error prog.
- -
-Definition Stuck (σ : store * IMP) : Prop :=
-  ~progress σ.
- -
-Definition Reach '(p : IMP) '(σ : store * IMP) : Prop :=
-  exists V0, steps (V0, p) σ.
- -
-Definition HasBug (p : IMP) : Prop :=
-  exists σ, Reach p σ /\ Stuck σ.
- -
-Definition IsBug (p : IMP) (σ : store * IMP) : Prop :=
-  Reach p σ /\ Stuck σ.
- -
-Definition BadInput (p : IMP) (V0 : store) : Prop :=
-  exists σ, steps (V0, p) σ /\ Stuck σ.
- -
-Lemma is_error_Stuck:
-  forall V p, is_error p = true <-> Stuck (V, p).
-Proof.
-  intros.
-  rewrite is_error_correct.
-  now rewrite error_state_error.
-Qed.
-
-
- -
- - - diff --git a/html/WiSE.lang.imprec.html b/html/WiSE.lang.imprec.html deleted file mode 100644 index c5f9d29..0000000 --- a/html/WiSE.lang.imprec.html +++ /dev/null @@ -1,520 +0,0 @@ - - - - - - - - - - - - - -
-
-

WiSE.lang.imprec

- -
-From Coq Require Import ZArith String Program.Equality.
-From WiSE Require Import relations.
- -
-
- -
-

IMPREC, An extension of IMP with procedures and recursion

- -
- -

Syntax

- -
-
- -
-Definition ident := string.
- -
-Inductive variable :=
-  | Local (x : ident)
-  | Global (x : ident).
- -
-
- -
-Expressions -
-
-Inductive aexpr : Type :=
-  | Var : variable -> aexpr
-  | Cst : Z -> aexpr
-  | Add : aexpr -> aexpr -> aexpr
-  | Sub : aexpr -> aexpr -> aexpr.
- -
-Inductive bexpr : Type :=
-  | Bcst : bool -> bexpr
-  | Ble : aexpr -> aexpr -> bexpr
-  | Beq : aexpr -> aexpr -> bexpr
-  | Bnot : bexpr -> bexpr
-  | Band : bexpr -> bexpr -> bexpr.
- -
-Definition Bor (b1 b2 : bexpr) := Band (Bnot b1) (Bnot b2).
- -
-
- -
-Commands -
-
-Inductive stmt : Type :=
-  | : stmt
-  | Ite : bexpr -> stmt -> stmt -> stmt
-  | Seq : stmt -> stmt -> stmt
-  | Aff : string -> aexpr -> stmt
-  | Err : stmt
-  | Loop : bexpr -> stmt -> stmt
-  .
- -
-Definition Assert c := Ite c Skip Err.
- -
-Fixpoint alocals (e : aexpr) (x : ident) : Prop :=
-  match e with
-  | Var (Local y) => y = x
-  | Var (Global _) | Cst _ => False
-  | Add e1 e2 | Sub e1 e2 => alocals e1 x \/ alocals e2 x
-  end.
- -
-Fixpoint blocals (b : bexpr) (x : ident) : Prop :=
-  match b with
-  | Bcst _ => False
-  | Bnot b => blocals b x
-  | Ble e1 e2 | Beq e1 e2 => alocals e1 x \/ alocals e2 x
-  | Band b1 b2 => blocals b1 x \/ blocals b2 x
-  end.
- -
-Fixpoint locals (s : stmt) (x : ident) : Prop :=
-  match s with
-  | Skip => False
-  | Ite b s1 s2 => blocals b x \/ locals s1 x \/ locals s2 x
-  | Seq s1 s2 => locals s1 x \/ locals s2 x
-  | Aff y e => x = y \/ alocals e x
-  | Err => False
-  | Loop b s => blocals b x \/ locals s x
-  end.
- -
-Record declaration := {
-  params : list ident;
-  body : stmt;
-  Hlocals : forall x, locals body x -> List.In x params
-}.
- -
-Record IMPREC := {
-  decls : list declaration;
-  main : stmt;
-}.
- -
-
- -
-NOTE : - Option 1 : assume programs are well formed -
    -
  • No undefined local variables - -
    • -
  • No references to undefined procedures - -
    • -
- Option 2 : Semantics fail if undefined variable.... - -
- - Opinion : -
    -
  • option1 is an approach that works well for static languages - -
    • -
  • option2 models more dynamic languages (python, js) - -
    • -
- -
- -

Semantics

- -
-
- -
-Definition global_store := ident -> Z.
-Definition local_store := ident -> Z.
- -
-
- -
-

Denotational semantics for expressions

- -
- - Semantics of Arithmetic expressions -
-
-Fixpoint aeval (gs : global_store) (ls : local_store) (e : aexpr) : Z :=
-  match e with
-  | Var (Global x) => gs x
-  | Var (Local x) => ls x
-  | Cst c => c
-  | Add e1 e2 => aeval gs ls e1 + aeval gs ls e2
-  | Sub e1 e2 => aeval gs ls e1 - aeval gs ls e2
-  end.
- -
-(* Fixpoint asubst (e : aexpr) (x : ident) (e' : aexpr) :=
-  match e with
-  | Var y => if (string_dec y x) then e' else e
-  | Cst _ => e
-  | Add e1 e2 => Add (asubst e1 x e') (asubst e2 x e')
-  | Sub e1 e2 => Sub (asubst e1 x e') (asubst e2 x e')
-  end.
-
-Definition ainst (e : aexpr) (x : ident) (vx : Z) :=
-  asubst e x (Cst vx).
-
-Fixpoint beval (s : store) (e : bexpr) : bool :=
-  match e with
-  | Bcst b      => b
-  | Ble e1 e2   => (aeval s e1 <? aeval s e2)Z
-  | Band e1 e2  => beval s e1 && beval s e2
-  | Bnot e      => negb (beval s e)
-  end.
-
-Fixpoint bsubst (e : bexpr) (x : ident) (e' : aexpr) :=
-  match e with
-  | Bcst _      => e
-  | Beq e1 e2   => Beq (asubst e1 x e') (asubst e2 x e')
-  | Ble e1 e2   => Ble (asubst e1 x e') (asubst e2 x e')
-  | Band e1 e2  => Band (bsubst e1 x e') (bsubst e2 x e')
-  | Bnot e      => Bnot (bsubst e x e')
-  end.
-
-Definition binst (e : bexpr) (x : ident) (vx : Z) :=
-  bsubst e x (Cst vx).
-
-(** *** Operational semantics of IMP *)
-
-(** Updating a store *)
-Definition update (s : store) (x : ident) (v : Z) : store :=
-  fun y => if string_dec y x then v else s y.
-
-(** Subtitution lemma (for arithmetic expressions) *)
-Lemma aeval_asubst :
-  forall s e x e',
-    aeval s (asubst e x e') = aeval (update s x (aeval s e')) e.
-Proof.
-  induction e; intros; simpl in *; auto.
-  - unfold update.
-    destruct (string_dec i x) eqn:E; auto.
-  - now rewrite IHe1, IHe2.
-  - now rewrite IHe1, IHe2.
-Qed.
-
-(** Subtitution lemma (for boolean expressions) *)
-Lemma beval_bsubst :
-  forall s c x e,
-    beval s (bsubst c x e) = beval (update s x (aeval s e)) c.
-Proof.
-  intros. induction c; simpl in *; auto.
-  all: try now do 2 rewrite <- aeval_asubst.
-  now rewrite IHc.
-  now rewrite IHc1, IHc2.
-Qed.
-
-Lemma aeval_inst:
-  forall s e x vx, aeval (update s x vx) e = aeval s (ainst e x vx).
-Proof.
-  intros. unfold ainst.
-  now rewrite aeval_asubst.
-Qed.
-
-Lemma beval_inst:
-  forall s c x vx, beval (update s x vx) c = beval s (binst c x vx).
-Proof.
-  intros. induction c; simpl; auto.
-  all: try now do 2 rewrite aeval_inst.
-  now rewrite IHc.
-  now rewrite IHc1, IHc2.
-Qed.
-
-(** Big step semantics *)
-Inductive exec : store -> IMP -> store -> Prop :=
-  | exec_Skip s :
-    exec s Skip s
-  | exec_Aff s x e ve :
-    aeval s e = ve ->
-    exec s (Aff x e) (update s x ve)
-  | exec_Seq s s' s'' c1 c2 :
-    exec s c1 s' ->
-    exec s' c2 s'' ->
-    exec s (Seq c1 c2) s''
-  | exec_Ite_true s s' e c1 c2 :
-    beval s e = true ->
-    exec s c1 s' ->
-    exec s (Ite e c1 c2) s'
-  | exec_Ite_false s s' e c1 c2 :
-    beval s e = false ->
-    exec s c2 s' ->
-    exec s (Ite e c1 c2) s'
-  | exec_loop_true s s' s'' e c :
-    beval s e = true ->
-    exec s c s' ->
-    exec s' (Loop e c) s'' ->
-    exec s (Loop e c) s''
-  | exec_loop_false s e c :
-    beval s e = false ->
-    exec s (Loop e c) s.
-
-(** Small step semantics *)
-Inductive step : (store * IMP) -> (store * IMP) -> Prop :=
-  | step_Aff s x e ve :
-    aeval s e = ve -> step (s, Aff x e) (update s x ve, Skip)
-  | step_Seq s1 s2 c1 c2 c3 :
-    step (s1, c1) (s2, c2) -> step (s1, Seq c1 c3) (s2, Seq c2 c3)
-  | step_Seq_Skip s c :
-    step (s, Seq Skip c) (s, c)
-  | step_Ite_true s e c1 c2 :
-    beval s e = true -> step (s, Ite e c1 c2) (s, c1)
-  | step_Ite_false s e c1 c2 :
-    beval s e = false -> step (s, Ite e c1 c2) (s, c2)
-  | step_Loop_true s e c :
-    beval s e = true -> step (s, Loop e c) (s, Seq c (Loop e c))
-  | step_Loop_false s e c :
-    beval s e = false -> step (s, Loop e c) (s, Skip).
-
-Lemma aeval_stable:
-  forall env1 env2 e,
-    (forall x, env1 x = env2 x) ->
-    aeval env1 e = aeval env2 e.
-Proof.
-  intros.
-  induction e; simpl; auto.
-  - now rewrite IHe1, IHe2.
-  - now rewrite IHe1, IHe2.
-Qed.
-
-(** Sequences of steps *)
-Definition steps := star step.
-
-(** Taking several steps to the left of a sequence *)
-Lemma steps_seq :
-  forall s1 s2 c1 c2 c3,
-    steps (s1, c1) (s2, c2) -> steps (s1, Seq c1 c3) (s2, Seq c2 c3).
-Proof.
-  intros * H. dependent induction H.
-  * reflexivity.
-  * destruct y as s1' c1'.
-    eapply star_step. apply step_Seq, H.
-    now apply IHstar.
-Qed.
-
-(**
-  If a program p starting in state s terminates in 
-  state s' then p can take a sequence of steps
-  from s to s'
-*)
-Theorem exec_steps :
-  forall p s s', exec s p s' -> steps (s, p) (s', Skip).
-Proof.
-  induction 1.
-  - reflexivity.
-  - eapply star_step.
-    + apply (step_Aff _ _ _ _ H).
-    + reflexivity.
-  - etransitivity. apply steps_seq, IHexec1.
-    eapply star_step. apply step_Seq_Skip.
-    apply IHexec2.
-  - eapply star_step. eapply (step_Ite_true _ _ _ _ H).
-    apply IHexec.
-  - eapply star_step. eapply (step_Ite_false _ _ _ _ H).
-    apply IHexec.
-  - eapply star_step. eapply (step_Loop_true _ _ _ H).
-    etransitivity. eapply (steps_seq _ _ _ _ _ IHexec1).
-    eapply star_step. eapply step_Seq_Skip. apply IHexec2.
-  - eapply star_step. eapply (step_Loop_false _ _ _ H).
-    reflexivity.
-Qed.
-
-Theorem step_exec_exec :
-  forall c1 c2 s1 s2 s3,
-    step (s1, c1) (s2, c2) ->
-    exec s2 c2 s3 ->
-    exec s1 c1 s3.
-Proof.
-  intros * H1. generalize s3. clear s3.
-  dependent induction H1; intros.
-  - inversion_clear H.
-    now apply exec_Aff.
-  - inversion_clear H.
-    eapply exec_Seq; eauto.
-  - eapply exec_Seq; eauto using exec.
-  - eapply exec_Ite_true; eauto.
-  - eapply exec_Ite_false; eauto.
-  - inversion_clear H0.
-    eapply exec_loop_true; eauto.
-  - inversion H0; subst.
-    eapply exec_loop_false; eauto.
-Qed.
-
-(**
-  If a program p can take a sequence of steps
-  from s to s' then p terminates in
-  state s' when executed in s
-*)
-Theorem steps_exec :
-  forall p s s', steps (s, p) (s', Skip) -> exec s p s'.
-Proof.
-  intros. dependent induction H.
-  - apply exec_Skip.
-  - destruct y as s1 p1.
-    eapply step_exec_exec; eauto.
-Qed.
-
-(** ** Progression and Erroneous States  *)
-
-(** A configuration is said to progress if it is a Skip statement or
-    if it can take a step
-*)
-Definition progress '((s, p) : (store * IMP)) : Prop :=
-  p = Skip \/ exists s' p', step (s, p) (s', p').
-
-(** An error state is a state that can't progress *)
-Definition error_state (st : (store * IMP)) : Prop :=
-  ~progress st.
-
-(** Skip can progress *)
-Theorem progress_Skip:
-  forall env, progress (env, Skip).
-Proof.
-  now left.
-Qed.
-
-(** Ite can progress *)
-Theorem progress_Ite:
-  forall env b p1 p2, progress (env, Ite b p1 p2).
-Proof.
-  intros *. right.
-  destruct (beval env b) eqn:Hsat.
-  * exists env, p1. now econstructor.
-  * exists env, p2. now econstructor.
-Qed.
-
-(** Aff can progress *)
-Theorem progress_Aff:
-  forall env x e, progress (env, Aff x e).
-Proof.
-  intros *. right.
-  repeat econstructor.
-Qed.
-
-(** Aff can progress *)
-Theorem progress_Seq:
-  forall env p1 p2, progress (env, p1) -> progress (env, Seq p1 p2).
-Proof.
-  intros * -> | (s' & p' & H).
-  - right. exists env, p2. econstructor.
-  - right. exists s', (Seq p' p2). now econstructor.
-Qed.
-
-(** Loop can progress *)
-Theorem progress_Loop:
-  forall env b p, progress (env, Loop b p).
-Proof.
-  intros *. right.
-  destruct (beval env b) eqn:Hsat.
-  - exists env. now repeat econstructor.
-  - exists env, Skip. now repeat econstructor.
-Qed.
-
-(** If a sequence Seq p1 p2 can't progress, then p1 can't progress *)
-Theorem error_state_seq:
-  forall s p1 p2, error_state (s, Seq p1 p2) -> error_state (s, p1).
-Proof.
-  intros * H Hcontr.
-  apply H, progress_Seq, Hcontr.
-Qed.
-
-(** Syntactic characterization of error states *)
-Inductive error : IMP -> Prop :=
-  | error_Err : error Err
-  | error_Seq p1 p2 : error p1 -> error (Seq p1 p2).
-
-Theorem error_state_error :
-  forall s p, error_state (s, p) <-> error p.
-Proof.
-  intros. split.
-  - intros Hcontr.
-    induction p; try easy.
-    + now specialize (Hcontr (progress_Skip s)).
-    + now specialize (Hcontr (progress_Ite s _ _ _)).
-    + apply error_state_seq in Hcontr.
-      specialize (IHp1 Hcontr). now econstructor.
-    + now specialize (Hcontr (progress_Aff s _ _)).
-    + econstructor.
-    + now specialize (Hcontr (progress_Loop s _ _)).
-  - induction 1.
-    + intros H | (s' & p' & H); try easy.
-    + intros H' | (s' & p' & H'); try easy.
-      inversion H'; subst.
-      assert (Hprog : progress (s, p1)) by (right; repeat econstructor; eauto).
-      apply (IHerror Hprog).
-      inversion H.
-Qed.
-
-(** Executable check for erroneous state *)
-Fixpoint is_error (p : IMP) : bool :=
-  match p with
-  | Err => true
-  | Seq p _ => is_error p
-  | _ => false
-  end.
-
-Theorem is_error_correct:
-  forall p, is_error p = true <-> error p.
-Proof.
-  induction p; try easy.
-  - split.
-    + intros H*)
-
- -
- - - diff --git a/html/WiSE.relations.html b/html/WiSE.relations.html deleted file mode 100644 index fb33822..0000000 --- a/html/WiSE.relations.html +++ /dev/null @@ -1,158 +0,0 @@ - - - - - - - - - - - - - -
-
-

WiSE.relations

- -
-From Coq Require Import Classes.RelationClasses.
- -
-Section Sequences.
- -
-Variable A : Type.
-Variable R : A -> A -> Prop.
- -
-Inductive star : A -> A -> Prop :=
-  | star_refl x :
-    star x x
-  | star_step x y z :
-    R x y -> star y z -> star x z.
- -
-Lemma star_one :
-  forall x y, R x y -> star x y.
-Proof.
-  intros * H.
-  eapply (star_step _ _ _ H); auto.
-  apply star_refl.
-Qed.
- -
-Global Instance star_reflexive :
-  Reflexive star.
-Proof.
-  intros x. apply star_refl.
-Qed.
- -
-Global Instance star_trans :
-  Transitive star.
-Proof.
-  intros x y z H1 H2.
-  induction H1 in z, H2 |-*; auto.
-  apply (star_step _ _ _ H).
-  apply (IHstar _ H2).
-Qed.
- -
-Inductive starr: A -> A -> Prop :=
-  | starr_refl x :
-    starr x x
-  | starr_step x y z :
-    starr x y -> R y z -> starr x z.
- -
-Global Instance starr_trans :
-  Transitive starr.
-Proof.
-  intros x y z H1 H2.
-  induction H2; auto.
-  specialize (IHstarr H1).
-  econstructor; eauto.
-Qed.
- -
-Global Instance starr_reflexive :
-  Reflexive starr.
-Proof.
-  intros x. econstructor.
-Qed.
- -
-Theorem starr_star:
-  forall x y, star x y <-> starr x y.
-Proof.
-  intros. split; intros.
-  - induction H as [|? ? ? H1 H2 IH].
-    + apply starr_refl.
-    + etransitivity; eauto.
-      now repeat econstructor.
-  - induction H as [|? ? ? H1 H2 IH].
-    + reflexivity.
-    + etransitivity; eauto.
-      now repeat econstructor.
-Qed.
- -
-End Sequences.
- -
-Section Simulation.
- -
-Definition simulation {A B}
-  (RA : A -> A -> Prop)
-  (RB : B -> B -> Prop)
-  (sim : A -> B -> Prop) : Prop :=
-  forall a1 a2, RA a1 a2 -> forall b1, sim a1 b1 -> exists b2, RB b1 b2 /\ sim a2 b2.
- -
-Theorem star_simulation {A B} (RA : A -> A -> Prop) (RB : B -> B -> Prop):
-  forall sim, simulation RA RB sim -> simulation (star _ RA) (star _ RB) sim.
-Proof.
-  intros * H.
-  refine (star_ind _ _ _ _ _).
-  - intros a1 b1 H1. now exists b1.
-  - intros a1 a2 a3 Ha1 Ha2 IH b1 Hsim1.
-    specialize (H _ _ Ha1 _ Hsim1) as (b2 & Hb1 & Hsim2).
-    specialize (IH b2 Hsim2) as (b3 & Hb2 & Hsim3).
-    exists b3; split; auto.
-    etransitivity; eauto.
-    now apply star_one.
-Qed.
- -
-End Simulation.
- -
-Arguments star {_}.
-Arguments star_step {_} {_}.
-Arguments star_refl {_} {_}.
-Arguments star_one {_} {_}.
-Arguments star_reflexive {_} {_}.
-Arguments star_trans {_} {_}.
-
-
- -
- - - diff --git a/html/WiSE.streams.html b/html/WiSE.streams.html deleted file mode 100644 index 25078f4..0000000 --- a/html/WiSE.streams.html +++ /dev/null @@ -1,392 +0,0 @@ - - - - - - - - - - - - - -
-
-

WiSE.streams

- -
-From Coq Require Import List Lia.
-From WiSE Require Import equalities.
-Import ListNotations.
- -
-
- -
-

A library to manipulate infinite streams

- -
-
- -
-CoInductive stream (A : Type) : Type :=
-  | scons (x : A) (xs : stream A) : stream A.
-Arguments scons { _ }.
- -
-Definition force {A} (s : stream A) : stream A :=
-  match s with
-  | scons x xs => scons x xs
-  end.
- -
-Lemma force_id:
-  forall A (s : stream A), force s = s.
-Proof.
-  intros. now destruct s.
-Qed.
- -
-Ltac force :=
-  rewrite <- force_id; simpl force.
- -
-
- -
-Get the nth element of a stream -
-
-Fixpoint get {A} (n : nat) (s : stream A) : A :=
-  match n, s with
-  | 0, scons x _ => x
-  | S n, scons _ xs => get n xs
-  end.
- -
-Fixpoint shift {A} (n : nat) (s : stream A) : stream A :=
-  match n, s with
-  | 0, _ => s
-  | S n, scons _ xs => shift n xs
-  end.
- -
-Lemma get_shift:
-  forall A (s : stream A) n m, get n (shift m s) = get (n + m) s.
-Proof.
-  intros *.
-  induction m in s |-*.
-  - now replace (n + 0) with n by lia.
-  - simpl. destruct s. rewrite IHm.
-    now replace (n + S m) with (S (n + m)) by lia.
-Qed.
- -
-Lemma shift_eq:
-  forall A n (x : A) xs, shift (S n) (scons x xs) = shift n xs.
-Proof.
-  auto.
-Qed.
- -
-
- -
-Peek the first n elements of a stream -
-
-Fixpoint peek {A} (n : nat) (s : stream A) : list A :=
-  match n, s with
-  | 0, _ => []
-  | S n, scons x xs => x::peek n xs
-  end.
- -
-
- -
-Apply a function to a stream elementwise -
-
-CoFixpoint map {A B} (f : A -> B) (s : stream A) : stream B :=
-  match s with
-  | scons x xs => scons (f x) (map f xs)
-  end.
- -
-Lemma map_eq:
-  forall A B (f : A -> B) x xs, map f (scons x xs) = scons (f x) (map f xs).
-Proof.
-  intros. now rewrite <- force_id at 1.
-Qed.
- -
-
- -
-Filter out some element of a stream -
-
-CoFixpoint filter {A} (f : A -> bool) (s : stream A) : stream (option A) :=
-  match s with
-  | scons x xs =>
-    if f x then scons None (filter f xs)
-    else scons (Some x) (filter f xs)
-  end.
- -
-
- -
-Correctness of filter -
-
-Lemma get_filter :
-  forall A (f : A -> bool) (s : stream A) n,
-    if f (get n s) then
-      get n (filter f s) = None
-    else
-      get n (filter f s) = Some (get n s).
-Proof.
-  intros A f s n.
-  induction n in s |-*.
-  - simpl. now destruct s, (f x).
-  - destruct s; simpl.
-    destruct (f (get n s)) eqn:Heq.
-    + specialize (IHn s). rewrite Heq in IHn.
-      now destruct (f x).
-    + specialize (IHn s). rewrite Heq in IHn.
-      now destruct (f x).
-Qed.
- -
-Lemma get_map :
-  forall n A B (f : A -> B) (s : stream A),
-      get n (map f s) = f (get n s).
-Proof.
-  induction n.
-  - now destruct s.
-  - destruct s. simpl in *. now rewrite IHn.
-Qed.
- -
-
- -
-

Predicates Over Streams

- -
-
- -
-Module LTL.
-  Lemma shift_shift:
-    forall A m n (str : stream A), shift n (shift m str) = shift (n + m) str.
-  Proof.
-    induction m; auto.
-    - intros. now replace (n + 0) with n by lia.
-    - intros n str. replace (n + S m) with (S (n + m)) by lia.
-      destruct str. rewrite shift_eq.
-      now rewrite IHm.
-  Qed.
-  Definition t {A} : Type := (stream A -> Prop).
-  Definition now {A} (P : A -> Prop) : t :=
-    fun (s : stream A) => P (get 0 s).
-  Definition globally {A} (P : t) : t :=
-    fun (s : stream A) => forall n, P (shift n s).
-  Definition eventually {A} (P : t) : t :=
-    fun (s : stream A) => exists n, P (shift n s).
-  Definition imp {A} (P Q : t) : t :=
-    fun (s : stream A) => P s -> Q s.
-  Definition or {A} (P Q : t) : t :=
-    fun (s : stream A) => P s \/ Q s.
-  Definition and {A} (P Q : t) : t :=
-    fun (s : stream A) => P s /\ Q s.
-  Definition not {A} (P : t) : t :=
-    fun (s : stream A) => ~P s.
-  Definition next {A} (P : t) : t :=
-    fun (s : stream A) => P (shift 1 s).
- -
-  Notation "□ P" := (globally P) (at level 80).
-  Notation "◊ P" := (eventually P) (at level 80).
-  Notation "◯ P" := (next P) (at level 80).
-  Notation "P → Q" := (imp P Q) (at level 80).
-  Notation "¬ Q" := (not Q) (at level 80).
-  Notation "P ∨ Q" := (or P Q) (at level 80).
-  Notation "P ∧ Q" := (and P Q) (at level 80).
-  Notation "! P" := (now P) (at level 80).
-  Notation "!! p" := (! (fun x => x = p)) (at level 80).
-  Check (_ → (□ ◯ _)).
- -
-  Theorem globally_map:
-    forall A B (f : A -> B) (P : B -> Prop) str,
-      (□ (now (fun x => P (f x)))) str ->
-      (□ (now P)) (map f str).
-  Proof.
-    intros * H n.
-    specialize (H n).
-    unfold now in *. rewrite get_shift in *.
-    simpl in *.
-    now rewrite get_map.
-  Qed.
- -
-  Definition model {A} (s : stream A) (f : @t A) : Prop :=
-    f s.
-  Notation "α ⊨ φ" := (model α φ) (at level 80).
-End LTL.
- -
-
- -
-The current value satisfies P -
-
-Definition now {A} (s : stream A) (P : A -> Prop) : Prop :=
-  P (get 0 s).
- -
- -
-
- -
-Globally, P holds for all values of the stream -
-
-Definition globally {A} (s : stream A) (P : A -> Prop) : Prop :=
-  forall n, P (get n s).
- -
-
- -
-Eventually, a P value will be enumerated -
-
-Definition eventually {A} (s : stream A) (P : A -> Prop) : Prop :=
-  exists n, P (get n s).
- -
-
- -
-P holds untill Q holds -
-
-Definition untill {A} (s : stream A) (P Q : A -> Prop) :=
-  exists n, Q (get n s) /\ forall m, 0 <= m <= n -> P (get n s).
- -
-
- -
-

Examples

- -
- - Type of enumerators over a type A -
-
-Definition enum A : Type := nat -> A.
- -
-
- -
-Extensional equality of streams -
-
-Definition stream_equ {A} (s1 s2 : stream A) :=
-  forall n, get n s1 = get n s2.
- -
-
- -
-Extensional equality of enumerators -
-
-Definition enum_equ {A} (f1 f2 : enum A) :=
-  forall n, f1 n = f2 n.
- -
-
- -
-Instances of Eq -
-
-Instance stream_Eq {A} : @Eq (stream A) := EQ _ stream_equ.
-Instance fun_Eq {A} : @Eq (enum A) := EQ _ enum_equ.
- -
-
- -
-Converting enumerators into streams -
-
-CoFixpoint func_to_stream {A} (n : nat) (f : nat -> A) : stream A :=
-  scons (f n) (func_to_stream (S n) f).
- -
-
- -
-Applying func_to_stream gives an equivalent stream -
-
-Lemma func_to_stream_correct {A} :
-  forall n (f : nat -> A) m,
-    get m (func_to_stream n f) = f (n + m).
-Proof.
-  intros.
-  induction m in n |-*.
-  - now replace (n + 0) with n by lia.
-  - simpl get. rewrite IHm.
-    now replace (n + S m) with (S n + m) by lia.
-Qed.
- -
-
- -
-stream A and enum A are isomorphic -
-
-Theorem stream_func_iso {A}:
-  stream A ≃ (enum A).
-Proof.
-  exists (fun x n => get n x), (func_to_stream 0).
-  split.
-  - intros x n.
-    now rewrite func_to_stream_correct.
-  - intros f n.
-    now rewrite func_to_stream_correct.
-Qed.
-
-
- -
- - - diff --git a/html/WiSE.symbolic.solver.html b/html/WiSE.symbolic.solver.html deleted file mode 100644 index 0d569cb..0000000 --- a/html/WiSE.symbolic.solver.html +++ /dev/null @@ -1,325 +0,0 @@ - - - - - - - - - - - - - -
-
-

WiSE.symbolic.solver

- -
-From WiSE Require Import imp.
-From Coq Require Import ZArith String Bool Lia.
- -
-
- -
-

A Naive Constraint Solver/simplifier

- -
- - Smart constructor to build an Add term -
-
-Definition mk_add (a1 : aexpr) (a2 : aexpr) : aexpr :=
-  match a1, a2 with
-  | Cst c1, Cst c2 => Cst (c1 + c2)%Z
-  | _, Sub a2_1 a2_2 =>
-    if aeq a1 a2_2 then a2_1
-    else Add a1 a2
-  | _, _ => Add a1 a2
-  end.
- -
-
- -
-Smart constructor to build a Sub term -
-
-Definition mk_sub (a1 : aexpr) (a2 : aexpr) : aexpr :=
-  match a1, a2 with
-  | Cst c1, Cst c2 => Cst (c1 - c2)%Z
-  | _, Add a2_1 a2_2 =>
-    if aeq a1 a2_1 then Sub (Cst 0) a2_2
-    else if aeq a1 a2_2 then Sub (Cst 0) a2_1
-    else Sub a1 a2
-  | _, _ => Sub a1 a2
-  end.
- -
-
- -
-Basic, non-exhaustive simplification of arithmetic expressions -
-
-Fixpoint asimp (a: aexpr) : aexpr :=
-  match a with
-  | Cst _ => a
-  | Var _ => a
-  | Add a b => mk_add (asimp a) (asimp b)
-  | Sub a b => mk_sub (asimp a) (asimp b)
-  end.
- -
-Lemma mk_add_correct:
-  forall env a1 a2, aeval env (Add a1 a2) = aeval env (mk_add a1 a2).
-Proof.
-  intros. Opaque aeq.
-  destruct a1, a2; simpl; auto.
-  all:
-    destruct aeq eqn:Heq; auto;
-    apply aeq_spec in Heq as <-; simpl; lia.
-Qed.
- -
-Lemma mk_sub_correct:
-  forall env a1 a2, aeval env (Sub a1 a2) = aeval env (mk_sub a1 a2).
-Proof.
-  intros. Opaque aeq.
-  destruct a1, a2; simpl; auto.
-  all:
-    destruct (aeq _ a2_1) eqn:Heq1; [
-      apply aeq_spec in Heq1 as <-; simpl; lia |
-    ];
-    destruct (aeq _ a2_2) eqn:Heq2; [
-      apply aeq_spec in Heq2 as <-; simpl; lia |
-    ]; reflexivity.
-Qed.
- -
-Theorem asimp_correct:
-  forall env a, aeval env a = aeval env (asimp a).
-Proof.
-  induction a; simpl; auto.
-  + rewrite IHa1, IHa2.
-    now rewrite <- mk_add_correct.
-  + rewrite IHa1, IHa2.
-    now rewrite <- mk_sub_correct.
-Qed.
- -
-Definition mk_and (b1 b2 : bexpr) : bexpr :=
-  match b1, b2 with
-  | Bcst false, _ | _, Bcst false => Bcst false (* Null Law *)
-  | Bcst true, _ => b2 (* Identity Law *)
-  | _, Bcst true => b1 (* Identity Law *)
-  | lhs, Bnot rhs =>
-    if beq lhs rhs
-    then Bcst false (* Inverse Law *)
-    else Band lhs (Bnot rhs)
-  | Bnot lhs, rhs =>
-    if beq lhs rhs
-    then Bcst false (* Inverse Law *)
-    else Band (Bnot lhs) rhs
-  | _, _ =>
-    if beq b1 b2
-    then b1 (* Idempotent Law *)
-    else Band b1 b2
-  end.
- -
-Definition mk_not (b : bexpr) : bexpr :=
-  match b with
-  | Bnot lhs => lhs
-  | Bcst true => Bcst false
-  | Bcst false => Bcst true
-  | lhs => Bnot lhs
-  end.
- -
-
- -
-Simplification of boolean formulas -
-
-Fixpoint bsimp (b : bexpr) : bexpr :=
-  match b with
-  | Bcst _ => b
-  | Band lhs rhs => mk_and (bsimp lhs) (bsimp rhs)
-  | Bnot lhs => mk_not (bsimp lhs)
-  | Ble x y =>
-    match asimp x, asimp y with
-    | Cst x, Cst y => Bcst (x <=? y)%Z
-    | x, y => Ble x y
-    end
-  | Beq x y =>
-    match asimp x, asimp y with
-    | Cst x, Cst y => Bcst (x =? y)%Z
-    | x, y => if aeq x y then Bcst true else Beq x y
-    end
-  end.
- -
-Lemma mk_and_correct:
-  forall env b1 b2,
-    beval env (Band b1 b2) = beval env (mk_and b1 b2).
-Proof.
-  intros. Opaque beq.
-  destruct b1, b2; simpl; auto.
-  all: try now destruct b.
-  all: try now destruct b, b0.
-  all: try now destruct b; rewrite Bool.andb_comm.
-  - destruct beq eqn:Heq1; auto.
-    apply beq_spec in Heq1 as [=->->].
-    now rewrite Bool.andb_diag.
-  - destruct beq eqn:Heq1; auto.
-    apply beq_spec in Heq1 as <-.
-    apply Bool.andb_negb_r.
-  - destruct beq eqn:Heq1; auto.
-    apply beq_spec in Heq1 as [=->->].
-    now rewrite Bool.andb_diag.
-  - destruct beq eqn:Heq1; auto.
-    apply beq_spec in Heq1 as <-.
-    apply Bool.andb_negb_r.
-  - destruct beq eqn:Heq1; auto.
-    apply beq_spec in Heq1 as ->.
-    apply Bool.andb_negb_l.
-  - destruct beq eqn:Heq1; auto.
-    apply beq_spec in Heq1 as ->.
-    apply Bool.andb_negb_l.
-  - destruct beq eqn:Heq1; auto.
-    apply beq_spec in Heq1 as <-; simpl.
-    rewrite Bool.negb_involutive.
-    apply Bool.andb_negb_l.
-  - destruct beq eqn:Heq1; auto.
-    apply beq_spec in Heq1 as ->; simpl.
-    apply Bool.andb_negb_l.
-  - destruct beq eqn:Heq1; auto.
-    apply beq_spec in Heq1 as <-; simpl.
-    apply Bool.andb_negb_r.
-  - destruct beq eqn:Heq1; auto.
-    apply beq_spec in Heq1 as [=->->].
-    now rewrite Bool.andb_diag.
-Qed.
- -
-Lemma mk_not_correct:
-  forall env b,
-    beval env (Bnot b) = beval env (mk_not b).
-Proof.
-  intros env []; simpl; auto.
-  - now destruct b.
-  - now rewrite Bool.negb_involutive.
-Qed.
- -
-
- -
-Correctness of bsimp -
-
-Lemma bsimp_correct:
-  forall env b,
-    beval env (bsimp b) = beval env b.
-Proof.
-  Opaque asimp aeq beq.
-  induction b; simpl; auto.
-  - destruct (asimp a) eqn:Heq1, (asimp a0) eqn:Heq2.
-    all: now rewrite (asimp_correct _ a), (asimp_correct _ a0), Heq1, Heq2.
-  - destruct (asimp a) eqn:Heq1, (asimp a0) eqn:Heq2.
-    all: try now rewrite (asimp_correct _ a), (asimp_correct _ a0), Heq1, Heq2.
-    destruct aeq eqn:Heq.
-    apply aeq_spec in Heq as [=->].
-    rewrite (asimp_correct _ a), (asimp_correct _ a0), Heq1, Heq2.
-    simpl. now rewrite Z.eqb_refl.
-    now rewrite (asimp_correct _ a), (asimp_correct _ a0), Heq1, Heq2.
-    destruct aeq eqn:Heq.
-    apply aeq_spec in Heq as [=->->].
-    rewrite (asimp_correct _ a), (asimp_correct _ a0), Heq1, Heq2.
-    simpl. now rewrite Z.eqb_refl.
-    now rewrite (asimp_correct _ a), (asimp_correct _ a0), Heq1, Heq2.
-    destruct aeq eqn:Heq.
-    apply aeq_spec in Heq as [=->->].
-    rewrite (asimp_correct _ a), (asimp_correct _ a0), Heq1, Heq2.
-    simpl. now rewrite Z.eqb_refl.
-    now rewrite (asimp_correct _ a), (asimp_correct _ a0), Heq1, Heq2.
-  - rewrite <- mk_not_correct; simpl.
-    now rewrite IHb.
-  - rewrite <- mk_and_correct; simpl.
-    now rewrite IHb1, IHb2.
-Qed.
- -
-Inductive sat : Type :=
-  | SAT
-  | UNSAT
-  | MAYBE.
- -
-
- -
-An extremely naive sover -
-
-Definition solver (b : bexpr) : sat :=
-  match bsimp b with
-  | Bcst true => SAT
-  | Bcst false => UNSAT
-  | _ => MAYBE
-  end.
- -
-
- -
-solver is correct (but absolutely not complete) -
-
-Lemma solver_correct:
-  forall b,
-    (solver b = UNSAT -> forall env, beval env b = false) /\
-    (solver b = SAT -> exists env, beval env b = true).
-Proof.
-  intros. split.
-  - intros H env. unfold solver in H.
-    destruct (bsimp b) eqn:Heq; try easy.
-    destruct b0; try easy.
-    now rewrite <- bsimp_correct, Heq.
-  - intros H. unfold solver in H.
-    destruct (bsimp b) eqn:Heq; try easy.
-    destruct b0; try easy.
-    exists (fun _ => 0%Z).
-    now rewrite <- bsimp_correct, Heq.
-Qed.
- -
-Definition is_sat (b : bexpr) : bool :=
-  match solver b with
-  | SAT => true
-  | _ => false
-  end.
-
-
- -
- - - diff --git a/html/WiSE.symbolic.symex.html b/html/WiSE.symbolic.symex.html deleted file mode 100644 index fd7f2a0..0000000 --- a/html/WiSE.symbolic.symex.html +++ /dev/null @@ -1,592 +0,0 @@ - - - - - - - - - - - - - -
-
-

WiSE.symbolic.symex

- -
-From Coq Require Import ZArith String Program.Equality Logic.FunctionalExtensionality.
-From WiSE Require Import lang.imp relations.
- -
-
- -
-

Simple Symbolic Execution for IMP

- -
- -

Symbolic Evaluation

- -
- - Symbolic stores are simply substitutions (of variable with expressions) -
-
-Definition sym_store :=
-  ident -> aexpr.
- -
-Definition id : sym_store := fun x => Var x.
- -
-
- -
-Update a symbolic store -
-
-Definition sym_update (s : sym_store) (x : ident) (e : aexpr) : sym_store :=
-  fun y => if (y =? x)%string then e else s y.
- -
-
- -
-Compose a store and a symbolic store -
-
-Definition comp (env : store) (s : sym_store) : store :=
-  fun x => aeval env (s x).
- -
-Infix "∘" := (comp) (at level 70, no associativity).
- -
-Lemma comp_id :
-  forall env, comp env id = env.
-Proof.
-  intros.
-  now apply functional_extensionality.
-Qed.
- -
-
- -
-Symbolic evaluation of arithmetic expressions -
-
-Fixpoint sym_aeval (s : sym_store) (e : aexpr) : aexpr :=
-  match e with
-  | Var x => s x
-  | Cst c => e
-  | Add e1 e2 => Add (sym_aeval s e1) (sym_aeval s e2)
-  | Sub e1 e2 => Sub (sym_aeval s e1) (sym_aeval s e2)
-  end.
- -
-
- -
-Symbolic evaluation of boolean expressions -
-
-Fixpoint sym_beval (s : sym_store) (e : bexpr) : bexpr :=
-  match e with
-  | Bcst b => e
-  | Ble e1 e2 => Ble (sym_aeval s e1) (sym_aeval s e2)
-  | Beq e1 e2 => Beq (sym_aeval s e1) (sym_aeval s e2)
-  | Band e1 e2 => Band (sym_beval s e1) (sym_beval s e2)
-  | Bnot e => Bnot (sym_beval s e)
-  end.
- -
-
- -
-Substitution lemma (arithmetic) -
-
-Lemma aeval_comp:
-  forall env senv e,
-    aeval (env ∘ senv) e = aeval env (sym_aeval senv e).
-Proof.
-  induction e; simpl; auto.
-  - now rewrite IHe1, IHe2.
-  - now rewrite IHe1, IHe2.
-Qed.
- -
-
- -
-Substitution lemma (boolean) -
-
-Lemma beval_comp:
-  forall env senv e,
-    beval (env ∘ senv) e = beval env (sym_beval senv e).
-Proof.
-  induction e; simpl; auto.
-  - now do 2 rewrite aeval_comp.
-  - now do 2 rewrite aeval_comp.
-  - now rewrite IHe.
-  - now rewrite IHe1, IHe2.
-Qed.
- -
-
- -
-Composing with an updated symbolic store is the same - as composing with the initial symbolic store and then - do a (regular) update - -
-
-Lemma comp_update:
-  forall env senv e x,
-    env ∘ (sym_update senv x (sym_aeval senv e)) =
-    update (env ∘ senv) x (aeval (env ∘ senv) e).
-Proof.
-  intros.
-  apply functional_extensionality. intros y.
-  unfold comp, sym_update, update.
-  destruct String.eqb; subst; auto.
-  fold (comp env senv).
-  now rewrite aeval_comp.
-Qed.
- -
-
- -
-

Symbolic Semantics

- -
- - A symbolic state is a path constraint expressed as a bexpr, - a symbolic store and a program to execute - -
-
-Definition sym_state := (bexpr * sym_store * IMP)%type.
- -
-
- -
-A small step symbolic semantics for IMP -
-
-Inductive sym_step : sym_state -> sym_state -> Prop :=
-  | sym_step_Aff s π x e ve :
-    sym_aeval s e = ve -> sym_step (π, s, Aff x e) (π, sym_update s x ve, Skip)
-  | sym_step_Seq π1 π2 s1 s2 c1 c2 c3 :
-    sym_step (π1, s1, c1) (π2, s2, c2) -> sym_step (π1, s1, Seq c1 c3) (π2, s2, Seq c2 c3)
-  | sym_step_Seq_Skip s c :
-    sym_step (s, Seq Skip c) (s, c)
-  | sym_step_Ite_true π s e c1 c2 :
-    sym_step (π, s, Ite e c1 c2) (Band π (sym_beval s e), s, c1)
-  | sym_step_Ite_false π s e c1 c2 :
-    sym_step (π, s, Ite e c1 c2) (Band π (Bnot (sym_beval s e)), s, c2)
-  | sym_step_Loop_true π s e c :
-    sym_step (π, s, Loop e c) (Band π (sym_beval s e), s, Seq c (Loop e c))
-  | sym_step_Loop_false π s e c :
-    sym_step (π, s, Loop e c) (Band π (Bnot (sym_beval s e)), s, Skip).
- -
-
- -
-Reflexive Transitive Closure of sym_step -
-
-Definition sym_steps := star sym_step.
- -
-
- -
-sym_step is sound with respect to step -
-
-Lemma sym_step_step:
-  forall env senv1 senv2 π1 π2 c1 c2,
-    sym_step (π1, senv1, c1) (π2, senv2, c2) ->
-    beval env π2 = true ->
-    step (env ∘ senv1, c1) (env ∘ senv2, c2).
-Proof.
-  intros.
-  dependent induction H; subst.
-  - rewrite comp_update.
-    now econstructor.
-  - econstructor.
-    simpl in H0.
-    now eapply IHsym_step.
-  - econstructor.
-  - simpl in H0.
-    apply Bool.andb_true_iff in H0 as [H1 H2].
-    econstructor.
-    now rewrite beval_comp.
-  - simpl in H0.
-    apply Bool.andb_true_iff in H0 as [H1 H2].
-    econstructor.
-    rewrite beval_comp.
-    now apply Bool.negb_true_iff in H2.
-  - simpl in H0.
-    apply Bool.andb_true_iff in H0 as [H1 H2].
-    econstructor.
-    now rewrite beval_comp.
-  - simpl in H0.
-    apply Bool.andb_true_iff in H0 as [H1 H2].
-    econstructor.
-    rewrite beval_comp.
-    now apply Bool.negb_true_iff in H2.
-Qed.
- -
-
- -
-Monotonicity of path constraints over 1 step -
-
-Lemma sym_step_path:
-  forall env π1 senv1 c1 π2 senv2 c2,
-    sym_step (π1, senv1, c1) (π2, senv2, c2) ->
-    beval env π2 = true ->
-    beval env π1 = true.
-Proof.
-  intros * H1 H2.
-  dependent induction H1; auto; simpl in *.
-  - eapply IHsym_step; eauto.
-  - now apply Bool.andb_true_iff in H2 as [H2 _].
-  - now apply Bool.andb_true_iff in H2 as [H2 _].
-  - now apply Bool.andb_true_iff in H2 as [H2 _].
-  - now apply Bool.andb_true_iff in H2 as [H2 _].
-Qed.
- -
-
- -
-Monotonicity of path constraints over 0 or more steps -
-
-Lemma sym_steps_path:
-  forall env X Y,
-    sym_steps X Y ->
-    forall π1 senv1 c1 π2 senv2 c2,
-      X = (π1, senv1, c1) ->
-      Y = (π2, senv2, c2) ->
-      beval env π2 = true ->
-      beval env π1 = true.
-Proof.
-  intros env.
-  refine (star_ind _ _ _ _ _).
-  - now intros * -> [=->->->] H.
-  - intros [[π1 senv1] c1] [[π2 senv2] c2] [[π3 senv3] c3].
-    intros H1 H2 H3 * [=<-<-<-] [=<-<-<-] H.
-    eapply sym_step_path; eauto.
-Qed.
- -
-
- -
-sym_steps is sound with respect to steps. - This lemma is an (equivalent) reformulation of sym_steps_steps - that makes the pattern of star''s induction principle explicit. - -
-
-Lemma sym_steps_steps_aux:
-  forall env X Y,
-    sym_steps X Y ->
-    forall senv1 senv2 π1 π2 c1 c2,
-      X = (π1, senv1, c1) ->
-      Y = (π2, senv2, c2) ->
-      beval env π2 = true ->
-      steps (env ∘ senv1, c1) (env ∘ senv2, c2).
-Proof.
-  intros env.
-  refine (star_ind _ _ _ _ _).
-  - intros * -> [=->->->] _.
-    reflexivity.
-  - intros [[π1 senv1] c1] [[π2 senv2] c2] [[π3 senv3] c3].
-    intros * H1 H2 IH * [=<-<-<-] [=<-<-<-] H3.
-    econstructor.
-    eapply sym_step_step; eauto.
-    eapply sym_steps_path; eauto.
-    eapply IH; auto.
-Qed.
- -
-
- -
-sym_steps is sound with respect to steps -
-
-Lemma sym_steps_steps:
-  forall env senv1 senv2 π1 π2 c1 c2,
-    sym_steps (π1, senv1, c1) (π2, senv2, c2) ->
-    beval env π2 = true ->
-    steps (comp env senv1, c1) (comp env senv2, c2).
-Proof.
-  intros * H1 H2.
-  eapply sym_steps_steps_aux; eauto.
-Qed.
- -
-
- -
-sym_step is a sound semantics to simulate initial execution paths -
-
-Lemma symex_sound:
-  forall π env senv p1 p2,
-    sym_steps (Bcst true, id, p1) (π, senv, p2) ->
-    beval env π = true ->
-    steps (env, p1) (comp env senv, p2).
-Proof.
-  intros * H1 H2.
-  pose proof sym_steps_steps env _ _ _ _ _ _ H1 H2.
-  now rewrite comp_id in H.
-Qed.
- -
-
- -
- A symbolic state ⟨π, senv, p⟩ is said to simulate a concrete state - ⟨env, p'⟩ wrt to initial store env0 iff env0 satisfies - the path constraint π, and p = p', and the concrete - store env is obtained by composing the initial store env0 and the - symbolic store senv. - -
-
-Definition sim (env0 : store) '((env, p') : store * IMP) '((π, senv, p) : sym_state) :=
-  beval env0 π = true /\ env = comp env0 senv /\ p = p'.
- -
-Notation "e @ s1 ≃ s2" := (sim e s1 s2) (at level 80).
- -
-
- -
-We can build a simulation diagram over step and sym_step: - For every step step p p' such that sim p q, there exists q' such - that sym_step q q' and sim q q'. - -
-
-Lemma step_simulation_diagram:
-  forall env0,
-    simulation step sym_step (sim env0).
-Proof.
-  intros env0.
-  refine (step_ind _ _ _ _ _ _ _ _).
-  - intros env x e ve <- [[π1 senv1] p1] (Hπ & -> & ->).
-    repeat econstructor; auto.
-    now rewrite comp_update.
-  - intros env1 env2 p1 p2 p3 Hstep IH [[π1 senv1] p1'] (Hπ & -> & ->).
-    assert (Hsim : sim env0 (comp env0 senv1, p1) (π1, senv1, p1)) by easy.
-    specialize (IH _ Hsim) as ([[π2 senv2] p2'] & H1 & (Hπ2 & -> & ->)).
-    repeat esplit.
-    + econstructor; apply H1.
-    + red; auto.
-  - intros env p [[π1 senv1] p1] (Hπ1 & -> & ->).
-    repeat esplit.
-    + apply sym_step_Seq_Skip.
-    + red; auto.
-  - intros env e p1 p2 He [[π1 senv1] p1'] (Hπ1 & -> & ->).
-    repeat esplit.
-    + apply sym_step_Ite_true.
-    + red; simpl. now rewrite <- beval_comp, He, Hπ1.
-  - intros env e p1 p2 He [[π1 senv1] p1'] (Hπ1 & -> & ->).
-    repeat esplit.
-    + apply sym_step_Ite_false.
-    + red; simpl. now rewrite <- beval_comp, He, Hπ1.
-  - intros env e p He [[π1 senv1] p1] (Hπ1 & -> & ->).
-    repeat esplit.
-    + apply sym_step_Loop_true.
-    + red; simpl. now rewrite <- beval_comp, He, Hπ1.
-  - intros env e p He [[π1 senv1] p1] (Hπ1 & -> & ->).
-    repeat esplit.
-    + apply sym_step_Loop_false.
-    + red; simpl. now rewrite <- beval_comp, He, Hπ1.
-Qed.
- -
-Lemma sim_init:
-  forall env p, env @ (env, p) ≃ (Bcst true, id, p).
-Proof.
-  easy.
-Qed.
- -
-
- -
-The simulation diagram step_simulation_diagram can - be iterated and therefore extended - to a diagram over steps and sym_steps - -
-
-Theorem steps_simulation_diagram:
-  forall env0,
-    simulation steps sym_steps (sim env0).
-Proof.
-  intros.
-  apply star_simulation, step_simulation_diagram.
-Qed.
- -
-Theorem symex_complete:
-  forall env p s,
-    steps (env, p) s ->
-    exists s',
-      sym_steps (Bcst true, id, p) s' /\
-      env @ s ≃ s'.
-Proof.
-  intros * H.
-  now eapply steps_simulation_diagram; eauto.
-Qed.
- -
-Definition potential_bug (s s' : sym_state) : Prop :=
-  let '(path, env, prog) := s' in
-  sym_steps s s' /\ error prog.
- -
-Definition relatively_sound_bug_finding:
-  forall prog0 path senv prog,
-    potential_bug (Bcst true, id, prog0) (path, senv, prog) ->
-    forall env0,
-      beval env0 path = true ->
-      imp.bug (env0, prog0) (env0 ∘ senv, prog).
-Proof.
-  intros * [H1 H2]. split; auto.
-  eapply symex_sound; eauto.
-Qed.
- -
-Definition complete_bug_finding:
-  forall env0 prog0 env1 prog1,
-    imp.bug (env0, prog0) (env1, prog1) ->
-    exists π senv prog,
-      potential_bug (Bcst true, id, prog0) (π, senv, prog) /\
-      sim env0 (env1, prog1) (π, senv, prog).
-Proof.
-  intros * [([[π senv] prog1] & [H1 [H2 [H3 H4]]])%symex_complete H5]; subst.
-  exists π, senv, prog2.
-  repeat split; auto.
-Qed.
- -
-Definition Reach '(p : IMP) '(σ : store * IMP) : Prop :=
-  exists V0, exists σ', sym_steps (Bcst true, id, p) σ' /\ V0 @ σ ≃ σ'.
- -
-Definition HasBug (p : IMP) : Prop :=
-  exists σ, Reach p σ /\ Stuck σ.
- -
-Definition IsBug (p : IMP) (σ : store * IMP) : Prop :=
-  Reach p σ /\ Stuck σ.
- -
-Definition BadInput (p : IMP) (V0 : store) : Prop :=
-  exists σ, exists σ', sym_steps (Bcst true, id, p) σ' /\ V0 @ σ ≃ σ' /\ Stuck σ.
- -
-Theorem Reach_sound:
-  forall p σ, Reach p σ -> imp.Reach p σ.
-Proof.
-  intros p0 [V p].
-  intros (V0 & [[φ S] p'] & [Hsteps [Heq1 [-> ->]]]).
-  exists V0.
-  rewrite <- (comp_id V0) at 1.
-  eapply sym_steps_steps; eauto.
-Qed.
- -
-Theorem Reach_complete:
-  forall p σ, imp.Reach p σ -> Reach p σ.
-Proof.
-  intros p0 [V p].
-  intros (V0 & Hsteps%symex_complete). red.
-  exists V0. apply Hsteps.
-Qed.
- -
-Theorem HasBug_correct:
-  forall p, HasBug p <-> imp.HasBug p.
-Proof.
-  intros p. split.
-  - intros [σ [Hreach%Reach_sound Hstuck]].
-    now exists σ.
-  - intros [σ [Hreach%Reach_complete Hstuck]].
-    now exists σ.
-Qed.
- -
-Theorem IsBug_correct:
-  forall p σ, IsBug p σ <-> imp.IsBug p σ.
-Proof.
-  intros p σ. split.
-  - now intros [Hreach%Reach_sound Hstuck].
-  - now intros [Hreach%Reach_complete Hstuck].
-Qed.
- -
-Theorem BadInput_correct:
-  forall p V0, BadInput p V0 <-> imp.BadInput p V0.
-Proof.
-  intros p0 V0. split.
-  - eintros ([V p] & [[φ S] p'] & [Hsteps [[Heq1 [-> ->]] Hstuck]]).
-    exists (V0 ∘ S, p). split; auto.
-    eapply symex_sound; eauto.
-  - eintros (σ & (σ' & Hsteps & Hequiv)%symex_complete & Hstuck).
-    now exists σ, σ'.
-Qed.
- -
-
- -
-What it means to be a concrete state denoted by - a symbolic state -
-
-Definition Concrete '(σ : sym_state) :=
-  fun σ' => exists V0, V0 @ σ' ≃ σ.
-
-
- -
- - - diff --git a/html/WiSE.utils.html b/html/WiSE.utils.html deleted file mode 100644 index f46df52..0000000 --- a/html/WiSE.utils.html +++ /dev/null @@ -1,104 +0,0 @@ - - - - - - - - - - - - - -
-
-

WiSE.utils

- -
-From Coq Require Import List.
-Import ListNotations.
- -
-
- -
-Reduce a list of optional values - to a single optional values. - -
-
-Fixpoint reduce {A} (f : A -> A -> A) (l : list (option A)) : option A :=
-  match l with
-  | [] => None
-  | None::_ => None
-  | [Some x] => Some x
-  | Some x::xs =>
-    option_map (fun y => f x y) (reduce f xs)
-  end.
- -
-
- -
-Apply f element-wise but fail if any of the applications of f returns None -
-
-Fixpoint map_opt {A B} (f : A -> option B) (l : list A) : option (list B) :=
-  match l with
-  | [] => None
-  | x::xs =>
-    match f x with
-    | None => None
-    | Some fx => option_map (fun xs => fx::xs) (map_opt f xs)
-    end
-  end.
- -
-
- -
-Check that a list of optional values does not contain None -
-
-Fixpoint all_some {A} (l : list (option A)) : option (list A) :=
-  match l with
-  | [] => Some []
-  | None::_ => None
-  | Some x::xs => option_map (fun xs => x::xs) (all_some xs)
-  end.
- -
-
- -
-Find the first Some element of a list of optional values -
-
-Fixpoint first {A} (l : list (option A)) : option A :=
-  match l with
-  | [] => None
-  | Some x::xs => Some x
-  | None::xs => first xs
-  end.
-
-
- -
- - - diff --git a/html/config.js b/html/config.js deleted file mode 100644 index 72be613..0000000 --- a/html/config.js +++ /dev/null @@ -1,72 +0,0 @@ -var coqdocjs = coqdocjs || {}; - -coqdocjs.repl = { - "forall": "∀", - "exists": "∃", - "~": "¬", - "/\\": "∧", - "\\/": "∨", - "->": "→", - "<-": "←", - "<->": "↔", - "=>": "⇒", - "<>": "≠", - "<=": "≤", - ">=": "≥", - "el": "∈", - "nel": "∉", - "<<=": "⊆", - "|-": "⊢", - ">>": "»", - "<<": "⊆", - "++": "⧺", - "===": "≡", - "=/=": "≢", - "=~=": "≅", - "==>": "⟹", - "lhd": "⊲", - "rhd": "⊳", - "nat": "ℕ", - "alpha": "α", - "beta": "β", - "gamma": "γ", - "delta": "δ", - "epsilon": "ε", - "eta": "η", - "iota": "ι", - "kappa": "κ", - "lambda": "λ", - "mu": "μ", - "nu": "ν", - "omega": "ω", - "phi": "ϕ", - "pi": "π", - "psi": "ψ", - "rho": "ρ", - "sigma": "σ", - "tau": "τ", - "theta": "θ", - "xi": "ξ", - "zeta": "ζ", - "Delta": "Δ", - "Gamma": "Γ", - "Pi": "Π", - "Sigma": "Σ", - "Omega": "Ω", - "Xi": "Ξ" -}; - -coqdocjs.subscr = { - "0" : "₀", - "1" : "₁", - "2" : "₂", - "3" : "₃", - "4" : "₄", - "5" : "₅", - "6" : "₆", - "7" : "₇", - "8" : "₈", - "9" : "₉", -}; - -coqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="]; diff --git a/html/coqdoc.css b/html/coqdoc.css deleted file mode 100644 index 18dad89..0000000 --- a/html/coqdoc.css +++ /dev/null @@ -1,197 +0,0 @@ -@import url(https://fonts.googleapis.com/css?family=Open+Sans:400,700); - -body{ - font-family: 'Open Sans', sans-serif; - font-size: 14px; - color: #2D2D2D -} - -a { - text-decoration: none; - border-radius: 3px; - padding-left: 3px; - padding-right: 3px; - margin-left: -3px; - margin-right: -3px; - color: inherit; - font-weight: bold; -} - -#main .code a, #main .inlinecode a, #toc a { - font-weight: inherit; -} - -a[href]:hover, [clickable]:hover{ - background-color: rgba(0,0,0,0.1); - cursor: pointer; -} - -h, h1, h2, h3, h4, h5 { - line-height: 1; - color: black; - text-rendering: optimizeLegibility; - font-weight: normal; - letter-spacing: 0.1em; - text-align: left; -} - -div + br { - display: none; -} - -div:empty{ display: none;} - -#main h1 { - font-size: 2em; -} - -#main h2 { - font-size: 1.667rem; -} - -#main h3 { - font-size: 1.333em; -} - -#main h4, #main h5, #main h6 { - font-size: 1em; -} - -#toc h2 { - padding-bottom: 0; -} - -#main .doc { - margin: 0; - text-align: justify; -} - -.inlinecode, .code, #main pre { - font-family: monospace; -} - -.code > br:first-child { - display: none; -} - -.doc + .code{ - margin-top:0.5em; -} - -.block{ - display: block; - margin-top: 5px; - margin-bottom: 5px; - padding: 10px; - text-align: center; -} - -.block img{ - margin: 15px; -} - -table.infrule { - border: 0px; - margin-left: 50px; - margin-top: 10px; - margin-bottom: 10px; -} - -td.infrule { - font-family: "Droid Sans Mono", "DejaVu Sans Mono", monospace; - text-align: center; - padding: 0; - line-height: 1; -} - -tr.infrulemiddle hr { - margin: 1px 0 1px 0; -} - -.infrulenamecol { - color: rgb(60%,60%,60%); - padding-left: 1em; - padding-bottom: 0.1em -} - -.id[type="constructor"], .id[type="projection"], .id[type="method"], -.id[title="constructor"], .id[title="projection"], .id[title="method"] { - color: #A30E16; -} - -.id[type="var"], .id[type="variable"], -.id[title="var"], .id[title="variable"] { - color: inherit; -} - -.id[type="definition"], .id[type="record"], .id[type="class"], .id[type="instance"], .id[type="inductive"], .id[type="library"], -.id[title="definition"], .id[title="record"], .id[title="class"], .id[title="instance"], .id[title="inductive"], .id[title="library"] { - color: #A6650F; -} - -.id[type="lemma"], -.id[title="lemma"]{ - color: #188B0C; -} - -.id[type="keyword"], .id[type="notation"], .id[type="abbreviation"], -.id[title="keyword"], .id[title="notation"], .id[title="abbreviation"]{ - color : #2874AE; -} - -.comment { - color: #808080; -} - -/* TOC */ - -#toc h2{ - letter-spacing: 0; - font-size: 1.333em; -} - -/* Index */ - -#index { - margin: 0; - padding: 0; - width: 100%; -} - -#index #frontispiece { - margin: 1em auto; - padding: 1em; - width: 60%; -} - -.booktitle { font-size : 140% } -.authors { font-size : 90%; - line-height: 115%; } -.moreauthors { font-size : 60% } - -#index #entrance { - text-align: center; -} - -#index #entrance .spacer { - margin: 0 30px 0 30px; -} - -ul.doclist { - margin-top: 0em; - margin-bottom: 0em; -} - -#toc > * { - clear: both; -} - -#toc > a { - display: block; - float: left; - margin-top: 1em; -} - -#toc a h2{ - display: inline; -} diff --git a/html/coqdocjs.css b/html/coqdocjs.css deleted file mode 100644 index d94bb58..0000000 --- a/html/coqdocjs.css +++ /dev/null @@ -1,249 +0,0 @@ -/* replace unicode */ - -.id[repl] .hidden { - font-size: 0; -} - -.id[repl]:before{ - content: attr(repl); -} - -/* folding proofs */ - -@keyframes show-proof { - 0% { - max-height: 1.2em; - opacity: 1; - } - 99% { - max-height: 1000em; - } - 100%{ - } -} - -@keyframes hide-proof { - from { - visibility: visible; - max-height: 10em; - opacity: 1; - } - to { - max-height: 1.2em; - } -} - -.proof { - cursor: pointer; -} -.proof * { - cursor: pointer; -} - -.proof { - overflow: hidden; - position: relative; - transition: opacity 1s; - display: inline-block; -} - -.proof[show="false"] { - max-height: 1.2em; - visibility: visible; - opacity: 0.3; -} - -.proof[show="false"][animate] { - animation-name: hide-proof; - animation-duration: 0.25s; -} - -.proof[show=true] { - animation-name: show-proof; - animation-duration: 10s; -} - -.proof[show="false"]:before { - position: absolute; - visibility: visible; - width: 100%; - height: 100%; - display: block; - opacity: 0; - content: "M"; -} -.proof[show="false"]:hover:before { - content: ""; -} - -.proof[show="false"] + br + br { - display: none; -} - -.proof[show="false"]:hover { - visibility: visible; - opacity: 0.5; -} - -#toggle-proofs[proof-status="no-proofs"] { - display: none; -} - -#toggle-proofs[proof-status="some-hidden"]:before { - content: "Show Proofs"; -} - -#toggle-proofs[proof-status="all-shown"]:before { - content: "Hide Proofs"; -} - - -/* page layout */ - -html, body { - height: 100%; - margin:0; - padding:0; -} - -@media only screen { /* no div with internal scrolling to allow printing of whole content */ - body { - display: flex; - flex-direction: column - } - - #content { - flex: 1; - overflow: auto; - display: flex; - flex-direction: column; - } -} - -#content:focus { - outline: none; /* prevent glow in OS X */ -} - -#main { - display: block; - padding: 16px; - padding-top: 1em; - padding-bottom: 2em; - margin-left: auto; - margin-right: auto; - max-width: 60em; - flex: 1 0 auto; -} - -.libtitle { - display: none; -} - -/* header */ -#header { - width:100%; - padding: 0; - margin: 0; - display: flex; - align-items: center; - background-color: rgb(21,57,105); - color: white; - font-weight: bold; - overflow: hidden; -} - - -.button { - cursor: pointer; -} - -#header * { - text-decoration: none; - vertical-align: middle; - margin-left: 15px; - margin-right: 15px; -} - -#header > .right, #header > .left { - display: flex; - flex: 1; - align-items: center; -} -#header > .left { - text-align: left; -} -#header > .right { - flex-direction: row-reverse; -} - -#header a, #header .button { - color: white; - box-sizing: border-box; -} - -#header a { - border-radius: 0; - padding: 0.2em; -} - -#header .button { - background-color: rgb(63, 103, 156); - border-radius: 1em; - padding-left: 0.5em; - padding-right: 0.5em; - margin: 0.2em; -} - -#header a:hover, #header .button:hover { - background-color: rgb(181, 213, 255); - color: black; -} - -#header h1 { padding: 0; - margin: 0;} - -/* footer */ -#footer { - text-align: center; - opacity: 0.5; - font-size: 75%; -} - -/* hyperlinks */ - -@keyframes highlight { - 50%{ - background-color: black; - } -} - -:target * { - animation-name: highlight; - animation-duration: 1s; -} - -a[name]:empty { - float: right; -} - -/* Proviola */ - -div.code { - width: auto; - float: none; -} - -div.goal { - position: fixed; - left: 75%; - width: 25%; - top: 3em; -} - -div.doc { - clear: both; -} - -span.command:hover { - background-color: inherit; -} diff --git a/html/coqdocjs.js b/html/coqdocjs.js deleted file mode 100644 index 10dc0bb..0000000 --- a/html/coqdocjs.js +++ /dev/null @@ -1,189 +0,0 @@ -var coqdocjs = coqdocjs || {}; -(function(){ - -function replace(s){ - var m; - if (m = s.match(/^(.+)'/)) { - return replace(m[1])+"'"; - } else if (m = s.match(/^([A-Za-z]+)_?(\d+)$/)) { - return replace(m[1])+m[2].replace(/\d/g, function(d){ - if (coqdocjs.subscr.hasOwnProperty(d)) { - return coqdocjs.subscr[d]; - } else { - return d; - } - }); - } else if (coqdocjs.repl.hasOwnProperty(s)){ - return coqdocjs.repl[s] - } else { - return s; - } -} - -function toArray(nl){ - return Array.prototype.slice.call(nl); -} - -function replInTextNodes() { - coqdocjs.replInText.forEach(function(toReplace){ - toArray(document.getElementsByClassName("code")).concat(toArray(document.getElementsByClassName("inlinecode"))).forEach(function(elem){ - toArray(elem.childNodes).forEach(function(node){ - if (node.nodeType != Node.TEXT_NODE) return; - var fragments = node.textContent.split(toReplace); - node.textContent = fragments[fragments.length-1]; - for (var k = 0; k < fragments.length - 1; ++k) { - node.parentNode.insertBefore(document.createTextNode(fragments[k]),node); - var replacement = document.createElement("span"); - replacement.appendChild(document.createTextNode(toReplace)); - replacement.setAttribute("class", "id"); - replacement.setAttribute("type", "keyword"); - node.parentNode.insertBefore(replacement, node); - } - }); - }); - }); -} - -function replNodes() { - toArray(document.getElementsByClassName("id")).forEach(function(node){ - if (["var", "variable", "keyword", "notation", "definition", "inductive"].indexOf(node.getAttribute("type"))>=0){ - var text = node.textContent; - var replText = replace(text); - if(text != replText) { - node.setAttribute("repl", replText); - node.setAttribute("title", text); - var hidden = document.createElement("span"); - hidden.setAttribute("class", "hidden"); - while (node.firstChild) { - hidden.appendChild(node.firstChild); - } - node.appendChild(hidden); - } - } - }); -} - -function isVernacStart(l, t){ - t = t.trim(); - for(var s of l){ - if (t == s || t.startsWith(s+" ") || t.startsWith(s+".")){ - return true; - } - } - return false; -} - -function isProofStart(n){ - return isVernacStart(["Proof"], n.textContent) || - (isVernacStart(["Next"], n.textContent) && isVernacStart(["Obligation"], n.nextSibling.nextSibling.textContent)); -} - -function isProofEnd(s){ - return isVernacStart(["Qed", "Admitted", "Defined", "Abort"], s); -} - -function proofStatus(){ - var proofs = toArray(document.getElementsByClassName("proof")); - if(proofs.length) { - for(var proof of proofs) { - if (proof.getAttribute("show") === "false") { - return "some-hidden"; - } - } - return "all-shown"; - } - else { - return "no-proofs"; - } -} - -function updateView(){ - document.getElementById("toggle-proofs").setAttribute("proof-status", proofStatus()); -} - -function foldProofs() { - var hasCommands = true; - var nodes = document.getElementsByClassName("command"); - if(nodes.length == 0) { - hasCommands = false; - console.log("no command tags found") - nodes = document.getElementsByClassName("id"); - } - toArray(nodes).forEach(function(node){ - if(isProofStart(node)) { - var proof = document.createElement("span"); - proof.setAttribute("class", "proof"); - - node.parentNode.insertBefore(proof, node); - if(proof.previousSibling.nodeType === Node.TEXT_NODE) - proof.appendChild(proof.previousSibling); - while(node && !isProofEnd(node.textContent)) { - proof.appendChild(node); - node = proof.nextSibling; - } - if (proof.nextSibling) proof.appendChild(proof.nextSibling); // the Qed - if (!hasCommands && proof.nextSibling) proof.appendChild(proof.nextSibling); // the dot after the Qed - - proof.addEventListener("click", function(proof){return function(e){ - if (e.target.parentNode.tagName.toLowerCase() === "a") - return; - proof.setAttribute("show", proof.getAttribute("show") === "true" ? "false" : "true"); - proof.setAttribute("animate", ""); - updateView(); - };}(proof)); - proof.setAttribute("show", "false"); - } - }); -} - -function toggleProofs(){ - var someProofsHidden = proofStatus() === "some-hidden"; - toArray(document.getElementsByClassName("proof")).forEach(function(proof){ - proof.setAttribute("show", someProofsHidden); - proof.setAttribute("animate", ""); - }); - updateView(); -} - -function repairDom(){ - // pull whitespace out of command - toArray(document.getElementsByClassName("command")).forEach(function(node){ - while(node.firstChild && node.firstChild.textContent.trim() == ""){ - console.log("try move"); - node.parentNode.insertBefore(node.firstChild, node); - } - }); - toArray(document.getElementsByClassName("id")).forEach(function(node){ - node.setAttribute("type", node.getAttribute("title")); - }); - toArray(document.getElementsByClassName("idref")).forEach(function(ref){ - toArray(ref.childNodes).forEach(function(child){ - if (["var", "variable"].indexOf(child.getAttribute("type")) > -1) - ref.removeAttribute("href"); - }); - }); - -} - -function fixTitle(){ - var url = "/" + window.location.pathname; - var basename = url.substring(url.lastIndexOf('/')+1, url.lastIndexOf('.')); - if (basename === "toc") {document.title = "Table of Contents";} - else if (basename === "indexpage") {document.title = "Index";} - else {document.title = basename;} -} - -function postprocess(){ - repairDom(); - replInTextNodes() - replNodes(); - foldProofs(); - document.getElementById("toggle-proofs").addEventListener("click", toggleProofs); - updateView(); -} - -fixTitle(); -document.addEventListener('DOMContentLoaded', postprocess); - -coqdocjs.toggleProofs = toggleProofs; -})(); diff --git a/html/extract.html b/html/extract.html deleted file mode 100644 index 3cfddeb..0000000 --- a/html/extract.html +++ /dev/null @@ -1,46 +0,0 @@ - - - - - - - - - - - - - -
-
-

extract

- -
-From Coq Require Import Extraction ExtrOcamlString ExtrOcamlBasic.
-From WiSE Require Import streams implem.bugfinder symbolic.solver.
- -
-Cd "./extraction".
-Extraction "loop.ml" find_bugs find_bugs_assuming peek bsimp.
-Cd "../".
-
-
- -
- - - diff --git a/html/indexpage.html b/html/indexpage.html deleted file mode 100644 index d4462d6..0000000 --- a/html/indexpage.html +++ /dev/null @@ -1,3052 +0,0 @@ - - - - - - - - - - - - - -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Global IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(986 entries)
Notation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(17 entries)
Binder IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(649 entries)
Module IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1 entry)
Variable IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(2 entries)
Library IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(11 entries)
Constructor IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(67 entries)
Lemma IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(81 entries)
Projection IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(6 entries)
Inductive IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(16 entries)
Instance IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(6 entries)
Section IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(5 entries)
Definition IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(122 entries)
Record IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(3 entries)
-
-

Global Index

-

A

-a [definition, in WiSE.implem.bugfinder]
-Add [constructor, in WiSE.lang.imprec]
-Add [constructor, in WiSE.lang.imp]
-aeq [definition, in WiSE.lang.imp]
-aeq_spec [lemma, in WiSE.lang.imp]
-aeval [definition, in WiSE.lang.imprec]
-aeval [definition, in WiSE.lang.imp]
-aeval_comp [lemma, in WiSE.symbolic.symex]
-aeval_stable [lemma, in WiSE.lang.imp]
-aeval_inst [lemma, in WiSE.lang.imp]
-aeval_asubst [lemma, in WiSE.lang.imp]
-aexpr [inductive, in WiSE.lang.imprec]
-aexpr [inductive, in WiSE.lang.imp]
-Aff [constructor, in WiSE.lang.imprec]
-Aff [constructor, in WiSE.lang.imp]
-ainst [definition, in WiSE.lang.imp]
-all_some [definition, in WiSE.utils]
-alocals [definition, in WiSE.lang.imprec]
-asimp [definition, in WiSE.symbolic.solver]
-asimp_correct [lemma, in WiSE.symbolic.solver]
-Assert [definition, in WiSE.lang.imprec]
-Assert [definition, in WiSE.lang.imp]
-asubst [definition, in WiSE.lang.imp]
-a0 [definition, in WiSE.implem.bugfinder]
-a1:1 [binder, in WiSE.symbolic.solver]
-a1:13 [binder, in WiSE.symbolic.solver]
-a1:16 [binder, in WiSE.symbolic.solver]
-a1:24 [binder, in WiSE.relations]
-a1:3 [binder, in WiSE.lang.imp]
-a1:5 [binder, in WiSE.symbolic.solver]
-a2:14 [binder, in WiSE.symbolic.solver]
-a2:17 [binder, in WiSE.symbolic.solver]
-a2:2 [binder, in WiSE.symbolic.solver]
-a2:25 [binder, in WiSE.relations]
-a2:4 [binder, in WiSE.lang.imp]
-a2:6 [binder, in WiSE.symbolic.solver]
-A:1 [binder, in WiSE.streams]
-A:1 [binder, in WiSE.equalities]
-A:1 [binder, in WiSE.utils]
-A:1 [binder, in WiSE.implem.bugfinder_proof]
-a:10 [binder, in WiSE.equalities]
-A:103 [binder, in WiSE.streams]
-A:106 [binder, in WiSE.streams]
-A:109 [binder, in WiSE.streams]
-A:11 [binder, in WiSE.streams]
-A:113 [binder, in WiSE.streams]
-A:117 [binder, in WiSE.streams]
-A:12 [binder, in WiSE.equalities]
-A:123 [binder, in WiSE.streams]
-A:124 [binder, in WiSE.streams]
-A:128 [binder, in WiSE.streams]
-A:132 [binder, in WiSE.streams]
-A:133 [binder, in WiSE.streams]
-A:134 [binder, in WiSE.streams]
-A:138 [binder, in WiSE.streams]
-A:14 [binder, in WiSE.utils]
-A:142 [binder, in WiSE.streams]
-A:17 [binder, in WiSE.streams]
-a:19 [binder, in WiSE.symbolic.solver]
-A:19 [binder, in WiSE.utils]
-A:19 [binder, in WiSE.relations]
-a:19 [binder, in WiSE.lang.imp]
-A:23 [binder, in WiSE.streams]
-A:27 [binder, in WiSE.streams]
-A:28 [binder, in WiSE.relations]
-A:31 [binder, in WiSE.streams]
-A:37 [binder, in WiSE.streams]
-A:4 [binder, in WiSE.equalities]
-A:43 [binder, in WiSE.streams]
-A:48 [binder, in WiSE.streams]
-A:53 [binder, in WiSE.streams]
-A:58 [binder, in WiSE.streams]
-A:6 [binder, in WiSE.streams]
-a:6 [binder, in WiSE.implem.bugfinder_proof]
-A:62 [binder, in WiSE.streams]
-A:66 [binder, in WiSE.streams]
-A:67 [binder, in WiSE.streams]
-A:7 [binder, in WiSE.utils]
-A:70 [binder, in WiSE.streams]
-A:74 [binder, in WiSE.streams]
-A:78 [binder, in WiSE.streams]
-a:8 [binder, in WiSE.lang.imp]
-A:82 [binder, in WiSE.streams]
-A:86 [binder, in WiSE.streams]
-a:9 [binder, in WiSE.symbolic.solver]
-A:9 [binder, in WiSE.streams]
-A:90 [binder, in WiSE.streams]
-A:93 [binder, in WiSE.streams]
-A:97 [binder, in WiSE.streams]
-

B

-b [definition, in WiSE.implem.bugfinder]
-BadInput [definition, in WiSE.symbolic.symex]
-BadInput [definition, in WiSE.lang.imp]
-BadInput_correct [lemma, in WiSE.symbolic.symex]
-Band [constructor, in WiSE.lang.imprec]
-Band [constructor, in WiSE.lang.imp]
-Bcst [constructor, in WiSE.lang.imprec]
-Bcst [constructor, in WiSE.lang.imp]
-Beq [constructor, in WiSE.lang.imprec]
-beq [definition, in WiSE.lang.imp]
-Beq [constructor, in WiSE.lang.imp]
-beq_spec [lemma, in WiSE.lang.imp]
-beval [definition, in WiSE.lang.imp]
-beval_comp [lemma, in WiSE.symbolic.symex]
-beval_inst [lemma, in WiSE.lang.imp]
-beval_bsubst [lemma, in WiSE.lang.imp]
-bexpr [inductive, in WiSE.lang.imprec]
-bexpr [inductive, in WiSE.lang.imp]
-bijection [definition, in WiSE.equalities]
-binst [definition, in WiSE.lang.imp]
-Ble [constructor, in WiSE.lang.imprec]
-Ble [constructor, in WiSE.lang.imp]
-blocals [definition, in WiSE.lang.imprec]
-Bnot [constructor, in WiSE.lang.imprec]
-Bnot [constructor, in WiSE.lang.imp]
-body [projection, in WiSE.lang.imprec]
-Bor [definition, in WiSE.lang.imprec]
-Bor [definition, in WiSE.lang.imp]
-bsimp [definition, in WiSE.symbolic.solver]
-bsimp_correct [lemma, in WiSE.symbolic.solver]
-bsubst [definition, in WiSE.lang.imp]
-bug [definition, in WiSE.lang.imp]
-bugfinder [library]
-bugfinder_proof [library]
-BugFound [constructor, in WiSE.implem.bugfinder]
-bug_found [definition, in WiSE.implem.bugfinder_proof]
-b0 [definition, in WiSE.implem.bugfinder]
-b1:12 [binder, in WiSE.lang.imp]
-b1:14 [binder, in WiSE.lang.imp]
-b1:20 [binder, in WiSE.symbolic.solver]
-b1:26 [binder, in WiSE.relations]
-b1:30 [binder, in WiSE.symbolic.solver]
-b1:9 [binder, in WiSE.lang.imprec]
-b2:10 [binder, in WiSE.lang.imprec]
-b2:13 [binder, in WiSE.lang.imp]
-b2:15 [binder, in WiSE.lang.imp]
-b2:21 [binder, in WiSE.symbolic.solver]
-b2:27 [binder, in WiSE.relations]
-b2:31 [binder, in WiSE.symbolic.solver]
-b:11 [binder, in WiSE.equalities]
-B:13 [binder, in WiSE.equalities]
-b:153 [binder, in WiSE.lang.imp]
-b:163 [binder, in WiSE.lang.imp]
-b:18 [binder, in WiSE.lang.imprec]
-B:2 [binder, in WiSE.implem.bugfinder_proof]
-B:20 [binder, in WiSE.relations]
-b:20 [binder, in WiSE.lang.imp]
-b:24 [binder, in WiSE.symbolic.solver]
-b:26 [binder, in WiSE.symbolic.solver]
-B:29 [binder, in WiSE.relations]
-b:33 [binder, in WiSE.symbolic.solver]
-b:35 [binder, in WiSE.symbolic.solver]
-b:38 [binder, in WiSE.symbolic.solver]
-B:38 [binder, in WiSE.streams]
-b:39 [binder, in WiSE.symbolic.solver]
-b:42 [binder, in WiSE.symbolic.solver]
-B:44 [binder, in WiSE.streams]
-B:5 [binder, in WiSE.equalities]
-b:5 [binder, in WiSE.implem.bugfinder_proof]
-B:59 [binder, in WiSE.streams]
-B:8 [binder, in WiSE.utils]
-b:9 [binder, in WiSE.lang.imp]
-B:98 [binder, in WiSE.streams]
-

C

-comp [definition, in WiSE.symbolic.symex]
-complete_bug_finding [definition, in WiSE.symbolic.symex]
-comp_update [lemma, in WiSE.symbolic.symex]
-comp_id [lemma, in WiSE.symbolic.symex]
-Concrete [definition, in WiSE.symbolic.symex]
-cond:29 [binder, in WiSE.implem.bugfinder]
-cond:31 [binder, in WiSE.implem.bugfinder]
-Cst [constructor, in WiSE.lang.imprec]
-Cst [constructor, in WiSE.lang.imp]
-c1:106 [binder, in WiSE.lang.imp]
-c1:113 [binder, in WiSE.lang.imp]
-c1:117 [binder, in WiSE.lang.imp]
-c1:131 [binder, in WiSE.lang.imp]
-c1:137 [binder, in WiSE.lang.imp]
-c1:39 [binder, in WiSE.symbolic.symex]
-c1:47 [binder, in WiSE.symbolic.symex]
-c1:52 [binder, in WiSE.symbolic.symex]
-c1:67 [binder, in WiSE.symbolic.symex]
-c1:72 [binder, in WiSE.symbolic.symex]
-c1:78 [binder, in WiSE.lang.imp]
-c1:81 [binder, in WiSE.symbolic.symex]
-c1:83 [binder, in WiSE.lang.imp]
-c1:88 [binder, in WiSE.lang.imp]
-c1:92 [binder, in WiSE.symbolic.symex]
-c1:99 [binder, in WiSE.symbolic.symex]
-c2:100 [binder, in WiSE.symbolic.symex]
-c2:107 [binder, in WiSE.lang.imp]
-c2:114 [binder, in WiSE.lang.imp]
-c2:118 [binder, in WiSE.lang.imp]
-c2:132 [binder, in WiSE.lang.imp]
-c2:138 [binder, in WiSE.lang.imp]
-c2:40 [binder, in WiSE.symbolic.symex]
-c2:48 [binder, in WiSE.symbolic.symex]
-c2:53 [binder, in WiSE.symbolic.symex]
-c2:68 [binder, in WiSE.symbolic.symex]
-c2:75 [binder, in WiSE.symbolic.symex]
-c2:79 [binder, in WiSE.lang.imp]
-c2:84 [binder, in WiSE.symbolic.symex]
-c2:84 [binder, in WiSE.lang.imp]
-c2:89 [binder, in WiSE.lang.imp]
-c2:93 [binder, in WiSE.symbolic.symex]
-c3:108 [binder, in WiSE.lang.imp]
-c3:133 [binder, in WiSE.lang.imp]
-c3:41 [binder, in WiSE.symbolic.symex]
-c:110 [binder, in WiSE.lang.imp]
-c:121 [binder, in WiSE.lang.imp]
-c:124 [binder, in WiSE.lang.imp]
-c:13 [binder, in WiSE.lang.imprec]
-c:23 [binder, in WiSE.lang.imp]
-c:43 [binder, in WiSE.symbolic.symex]
-c:57 [binder, in WiSE.symbolic.symex]
-c:57 [binder, in WiSE.lang.imp]
-c:61 [binder, in WiSE.symbolic.symex]
-c:65 [binder, in WiSE.lang.imp]
-c:94 [binder, in WiSE.lang.imp]
-c:97 [binder, in WiSE.lang.imp]
-

D

-declaration [record, in WiSE.lang.imprec]
-decls [projection, in WiSE.lang.imprec]
-display [definition, in WiSE.implem.bugfinder]
-done [definition, in WiSE.implem.bugfinder_proof]
-

E

-enum [definition, in WiSE.streams]
-enum_equ [definition, in WiSE.streams]
-env0:106 [binder, in WiSE.symbolic.symex]
-env0:114 [binder, in WiSE.symbolic.symex]
-env0:117 [binder, in WiSE.symbolic.symex]
-env0:129 [binder, in WiSE.symbolic.symex]
-env0:130 [binder, in WiSE.symbolic.symex]
-env1:125 [binder, in WiSE.lang.imp]
-env1:132 [binder, in WiSE.symbolic.symex]
-env2:126 [binder, in WiSE.lang.imp]
-env:10 [binder, in WiSE.implem.bugfinder]
-env:102 [binder, in WiSE.symbolic.symex]
-env:108 [binder, in WiSE.symbolic.symex]
-env:115 [binder, in WiSE.symbolic.symex]
-env:118 [binder, in WiSE.symbolic.symex]
-env:12 [binder, in WiSE.symbolic.solver]
-env:12 [binder, in WiSE.implem.bugfinder_proof]
-env:15 [binder, in WiSE.symbolic.solver]
-env:151 [binder, in WiSE.lang.imp]
-env:152 [binder, in WiSE.lang.imp]
-env:156 [binder, in WiSE.lang.imp]
-env:159 [binder, in WiSE.lang.imp]
-env:16 [binder, in WiSE.implem.bugfinder_proof]
-env:162 [binder, in WiSE.lang.imp]
-env:18 [binder, in WiSE.symbolic.symex]
-env:18 [binder, in WiSE.symbolic.solver]
-env:21 [binder, in WiSE.symbolic.symex]
-env:23 [binder, in WiSE.implem.bugfinder_proof]
-env:24 [binder, in WiSE.symbolic.symex]
-env:29 [binder, in WiSE.symbolic.solver]
-env:32 [binder, in WiSE.symbolic.solver]
-env:34 [binder, in WiSE.symbolic.solver]
-env:35 [binder, in WiSE.implem.bugfinder_proof]
-env:40 [binder, in WiSE.symbolic.solver]
-env:41 [binder, in WiSE.symbolic.solver]
-env:6 [binder, in WiSE.symbolic.symex]
-env:6 [binder, in WiSE.implem.bugfinder]
-env:62 [binder, in WiSE.symbolic.symex]
-env:69 [binder, in WiSE.symbolic.symex]
-env:76 [binder, in WiSE.symbolic.symex]
-env:8 [binder, in WiSE.implem.bugfinder_proof]
-env:85 [binder, in WiSE.symbolic.symex]
-env:9 [binder, in WiSE.symbolic.symex]
-env:94 [binder, in WiSE.symbolic.symex]
-Eq [record, in WiSE.equalities]
-EQ [constructor, in WiSE.equalities]
-equalities [library]
-eq_op [projection, in WiSE.equalities]
-Err [constructor, in WiSE.lang.imprec]
-Err [constructor, in WiSE.lang.imp]
-error [inductive, in WiSE.lang.imp]
-error_state_error [lemma, in WiSE.lang.imp]
-error_Seq [constructor, in WiSE.lang.imp]
-error_Err [constructor, in WiSE.lang.imp]
-error_state_seq [lemma, in WiSE.lang.imp]
-error_state [definition, in WiSE.lang.imp]
-eventually [definition, in WiSE.streams]
-Examples [section, in WiSE.implem.bugfinder]
-Examples.Gcd [section, in WiSE.implem.bugfinder]
-Bug _ [notation, in WiSE.implem.bugfinder]
-Examples.Simple [section, in WiSE.implem.bugfinder]
-exec [inductive, in WiSE.lang.imp]
-execute_gcd_err [definition, in WiSE.implem.bugfinder]
-execute_gcd_noerr [definition, in WiSE.implem.bugfinder]
-execute_gcd [definition, in WiSE.implem.bugfinder]
-exec_steps [lemma, in WiSE.lang.imp]
-exec_loop_false [constructor, in WiSE.lang.imp]
-exec_loop_true [constructor, in WiSE.lang.imp]
-exec_Ite_false [constructor, in WiSE.lang.imp]
-exec_Ite_true [constructor, in WiSE.lang.imp]
-exec_Seq [constructor, in WiSE.lang.imp]
-exec_Aff [constructor, in WiSE.lang.imp]
-exec_Skip [constructor, in WiSE.lang.imp]
-expand [definition, in WiSE.implem.bugfinder]
-expand_inv [lemma, in WiSE.implem.bugfinder_proof]
-expand_complete [lemma, in WiSE.implem.bugfinder_proof]
-expand_sound [lemma, in WiSE.implem.bugfinder_proof]
-extract [library]
-e':30 [binder, in WiSE.lang.imp]
-e':42 [binder, in WiSE.lang.imp]
-e':55 [binder, in WiSE.lang.imp]
-e:102 [binder, in WiSE.lang.imp]
-e:11 [binder, in WiSE.symbolic.symex]
-e:112 [binder, in WiSE.lang.imp]
-e:116 [binder, in WiSE.lang.imp]
-e:120 [binder, in WiSE.lang.imp]
-e:123 [binder, in WiSE.lang.imp]
-e:127 [binder, in WiSE.lang.imp]
-e:14 [binder, in WiSE.lang.imprec]
-e:15 [binder, in WiSE.symbolic.symex]
-e:158 [binder, in WiSE.lang.imp]
-e:20 [binder, in WiSE.symbolic.symex]
-e:23 [binder, in WiSE.symbolic.symex]
-e:25 [binder, in WiSE.lang.imp]
-e:26 [binder, in WiSE.symbolic.symex]
-e:28 [binder, in WiSE.lang.imp]
-e:33 [binder, in WiSE.symbolic.symex]
-e:33 [binder, in WiSE.lang.imp]
-e:36 [binder, in WiSE.lang.imprec]
-e:37 [binder, in WiSE.lang.imp]
-e:4 [binder, in WiSE.symbolic.symex]
-e:40 [binder, in WiSE.lang.imp]
-e:45 [binder, in WiSE.lang.imp]
-e:46 [binder, in WiSE.symbolic.symex]
-e:51 [binder, in WiSE.symbolic.symex]
-e:53 [binder, in WiSE.lang.imp]
-e:56 [binder, in WiSE.symbolic.symex]
-e:59 [binder, in WiSE.lang.imp]
-e:60 [binder, in WiSE.symbolic.symex]
-e:61 [binder, in WiSE.lang.imp]
-e:73 [binder, in WiSE.lang.imp]
-e:82 [binder, in WiSE.lang.imp]
-e:87 [binder, in WiSE.lang.imp]
-e:93 [binder, in WiSE.lang.imp]
-e:96 [binder, in WiSE.lang.imp]
-

F

-filter [definition, in WiSE.streams]
-find_bugs_complete [lemma, in WiSE.implem.bugfinder_proof]
-find_bugs_sound [lemma, in WiSE.implem.bugfinder_proof]
-find_bugs_assuming [definition, in WiSE.implem.bugfinder]
-find_bugs [definition, in WiSE.implem.bugfinder]
-Finished [constructor, in WiSE.implem.bugfinder]
-first [definition, in WiSE.utils]
-force [definition, in WiSE.streams]
-force_id [lemma, in WiSE.streams]
-func_to_stream_correct [lemma, in WiSE.streams]
-func_to_stream [definition, in WiSE.streams]
-fun_Eq [instance, in WiSE.streams]
-f1:129 [binder, in WiSE.streams]
-f2:130 [binder, in WiSE.streams]
-f:105 [binder, in WiSE.streams]
-f:136 [binder, in WiSE.streams]
-f:140 [binder, in WiSE.streams]
-f:16 [binder, in WiSE.equalities]
-f:2 [binder, in WiSE.utils]
-f:3 [binder, in WiSE.implem.bugfinder_proof]
-f:39 [binder, in WiSE.streams]
-f:45 [binder, in WiSE.streams]
-f:49 [binder, in WiSE.streams]
-f:54 [binder, in WiSE.streams]
-f:60 [binder, in WiSE.streams]
-f:8 [binder, in WiSE.equalities]
-f:9 [binder, in WiSE.utils]
-f:99 [binder, in WiSE.streams]
-

G

-gcd [definition, in WiSE.implem.bugfinder]
-gcd_buggy [definition, in WiSE.implem.bugfinder]
-gcd_assertions [definition, in WiSE.implem.bugfinder]
-get [definition, in WiSE.streams]
-get_map [lemma, in WiSE.streams]
-get_filter [lemma, in WiSE.streams]
-get_shift [lemma, in WiSE.streams]
-Global [constructor, in WiSE.lang.imprec]
-globally [definition, in WiSE.streams]
-global_store [definition, in WiSE.lang.imprec]
-gs:34 [binder, in WiSE.lang.imprec]
-g:17 [binder, in WiSE.equalities]
-g:9 [binder, in WiSE.equalities]
-

H

-HasBug [definition, in WiSE.symbolic.symex]
-HasBug [definition, in WiSE.lang.imp]
-HasBug_correct [lemma, in WiSE.symbolic.symex]
-here [definition, in WiSE.implem.bugfinder_proof]
-Hlocals [projection, in WiSE.lang.imprec]
-H0:15 [binder, in WiSE.equalities]
-H0:7 [binder, in WiSE.equalities]
-H:14 [binder, in WiSE.equalities]
-H:6 [binder, in WiSE.equalities]
-

I

-id [definition, in WiSE.symbolic.symex]
-ident [definition, in WiSE.lang.imprec]
-ident [definition, in WiSE.lang.imp]
-IMP [inductive, in WiSE.lang.imp]
-imp [library]
-IMPREC [record, in WiSE.lang.imprec]
-imprec [library]
-init [definition, in WiSE.implem.bugfinder]
-init_store' [definition, in WiSE.implem.bugfinder]
-init_store [definition, in WiSE.implem.bugfinder]
-init_assuming [definition, in WiSE.implem.bugfinder]
-IsBug [definition, in WiSE.symbolic.symex]
-IsBug [definition, in WiSE.lang.imp]
-IsBug_correct [lemma, in WiSE.symbolic.symex]
-isomorph [definition, in WiSE.equalities]
-is_sat [definition, in WiSE.symbolic.solver]
-is_error_Stuck [lemma, in WiSE.lang.imp]
-is_skip [definition, in WiSE.lang.imp]
-is_error_correct [lemma, in WiSE.lang.imp]
-is_error [definition, in WiSE.lang.imp]
-Ite [constructor, in WiSE.lang.imprec]
-Ite [constructor, in WiSE.lang.imp]
-

L

-Local [constructor, in WiSE.lang.imprec]
-locals [definition, in WiSE.lang.imprec]
-local_store [definition, in WiSE.lang.imprec]
-Loop [constructor, in WiSE.lang.imprec]
-Loop [constructor, in WiSE.lang.imp]
-ls:35 [binder, in WiSE.lang.imprec]
-LTL [module, in WiSE.streams]
-LTL.and [definition, in WiSE.streams]
-LTL.eventually [definition, in WiSE.streams]
-LTL.globally [definition, in WiSE.streams]
-LTL.globally_map [lemma, in WiSE.streams]
-LTL.imp [definition, in WiSE.streams]
-LTL.model [definition, in WiSE.streams]
-LTL.next [definition, in WiSE.streams]
-LTL.not [definition, in WiSE.streams]
-LTL.now [definition, in WiSE.streams]
-LTL.or [definition, in WiSE.streams]
-LTL.shift_shift [lemma, in WiSE.streams]
-LTL.t [definition, in WiSE.streams]
-_ ⊨ _ [notation, in WiSE.streams]
-_ ∧ _ [notation, in WiSE.streams]
-_ ∨ _ [notation, in WiSE.streams]
-_ → _ [notation, in WiSE.streams]
-!! _ [notation, in WiSE.streams]
-! _ [notation, in WiSE.streams]
-¬ _ [notation, in WiSE.streams]
-□ _ [notation, in WiSE.streams]
-◊ _ [notation, in WiSE.streams]
-◯ _ [notation, in WiSE.streams]
-l1:29 [binder, in WiSE.implem.bugfinder_proof]
-l1:32 [binder, in WiSE.implem.bugfinder_proof]
-l2:30 [binder, in WiSE.implem.bugfinder_proof]
-l2:33 [binder, in WiSE.implem.bugfinder_proof]
-l3:31 [binder, in WiSE.implem.bugfinder_proof]
-l3:37 [binder, in WiSE.implem.bugfinder_proof]
-l:10 [binder, in WiSE.utils]
-l:14 [binder, in WiSE.implem.bugfinder]
-l:15 [binder, in WiSE.utils]
-l:20 [binder, in WiSE.utils]
-l:21 [binder, in WiSE.implem.bugfinder_proof]
-l:27 [binder, in WiSE.implem.bugfinder_proof]
-l:3 [binder, in WiSE.utils]
-l:4 [binder, in WiSE.implem.bugfinder_proof]
-l:55 [binder, in WiSE.implem.bugfinder_proof]
-l:56 [binder, in WiSE.implem.bugfinder_proof]
-l:62 [binder, in WiSE.implem.bugfinder_proof]
-l:65 [binder, in WiSE.implem.bugfinder_proof]
-l:66 [binder, in WiSE.implem.bugfinder_proof]
-

M

-main [projection, in WiSE.lang.imprec]
-map [definition, in WiSE.streams]
-map_eq [lemma, in WiSE.streams]
-map_opt [definition, in WiSE.utils]
-map_in [lemma, in WiSE.implem.bugfinder_proof]
-MAYBE [constructor, in WiSE.symbolic.solver]
-mk_not_correct [lemma, in WiSE.symbolic.solver]
-mk_and_correct [lemma, in WiSE.symbolic.solver]
-mk_not [definition, in WiSE.symbolic.solver]
-mk_and [definition, in WiSE.symbolic.solver]
-mk_sub_correct [lemma, in WiSE.symbolic.solver]
-mk_add_correct [lemma, in WiSE.symbolic.solver]
-mk_sub [definition, in WiSE.symbolic.solver]
-mk_add [definition, in WiSE.symbolic.solver]
-my_prog [definition, in WiSE.implem.bugfinder]
-m:122 [binder, in WiSE.streams]
-m:141 [binder, in WiSE.streams]
-m:26 [binder, in WiSE.streams]
-m:63 [binder, in WiSE.streams]
-

N

-next_next:23 [binder, in WiSE.implem.bugfinder]
-next_next:17 [binder, in WiSE.implem.bugfinder]
-none [definition, in WiSE.implem.bugfinder_proof]
-now [definition, in WiSE.streams]
-n:112 [binder, in WiSE.streams]
-n:116 [binder, in WiSE.streams]
-n:12 [binder, in WiSE.streams]
-n:121 [binder, in WiSE.streams]
-n:127 [binder, in WiSE.streams]
-n:131 [binder, in WiSE.streams]
-n:135 [binder, in WiSE.streams]
-n:139 [binder, in WiSE.streams]
-n:144 [binder, in WiSE.streams]
-n:146 [binder, in WiSE.streams]
-n:18 [binder, in WiSE.streams]
-n:18 [binder, in WiSE.implem.bugfinder]
-n:25 [binder, in WiSE.streams]
-n:25 [binder, in WiSE.implem.bugfinder_proof]
-n:26 [binder, in WiSE.implem.bugfinder_proof]
-n:28 [binder, in WiSE.streams]
-n:28 [binder, in WiSE.implem.bugfinder_proof]
-n:32 [binder, in WiSE.streams]
-n:56 [binder, in WiSE.streams]
-n:57 [binder, in WiSE.streams]
-n:64 [binder, in WiSE.streams]
-n:73 [binder, in WiSE.streams]
-n:77 [binder, in WiSE.streams]
-

P

-params [projection, in WiSE.lang.imprec]
-path:11 [binder, in WiSE.implem.bugfinder_proof]
-path:126 [binder, in WiSE.symbolic.symex]
-path:15 [binder, in WiSE.implem.bugfinder_proof]
-path:22 [binder, in WiSE.implem.bugfinder_proof]
-path:34 [binder, in WiSE.implem.bugfinder_proof]
-path:7 [binder, in WiSE.implem.bugfinder_proof]
-path:7 [binder, in WiSE.implem.bugfinder]
-path:9 [binder, in WiSE.implem.bugfinder]
-pat:109 [binder, in WiSE.symbolic.symex]
-pat:113 [binder, in WiSE.symbolic.symex]
-pat:147 [binder, in WiSE.lang.imp]
-pat:8 [binder, in WiSE.implem.bugfinder]
-peek [definition, in WiSE.streams]
-Pending [constructor, in WiSE.implem.bugfinder]
-potential_bug [definition, in WiSE.symbolic.symex]
-potential_bug [definition, in WiSE.implem.bugfinder_proof]
-progress [definition, in WiSE.lang.imp]
-progress_Loop [lemma, in WiSE.lang.imp]
-progress_Seq [lemma, in WiSE.lang.imp]
-progress_Aff [lemma, in WiSE.lang.imp]
-progress_Ite [lemma, in WiSE.lang.imp]
-progress_Skip [lemma, in WiSE.lang.imp]
-prog0:125 [binder, in WiSE.symbolic.symex]
-prog0:131 [binder, in WiSE.symbolic.symex]
-prog1:133 [binder, in WiSE.symbolic.symex]
-prog:11 [binder, in WiSE.implem.bugfinder]
-prog:128 [binder, in WiSE.symbolic.symex]
-prog:13 [binder, in WiSE.implem.bugfinder_proof]
-prog:136 [binder, in WiSE.symbolic.symex]
-prog:17 [binder, in WiSE.implem.bugfinder_proof]
-prog:24 [binder, in WiSE.implem.bugfinder_proof]
-prog:36 [binder, in WiSE.implem.bugfinder_proof]
-prog:9 [binder, in WiSE.implem.bugfinder_proof]
-p':107 [binder, in WiSE.symbolic.symex]
-p':149 [binder, in WiSE.lang.imp]
-p1:104 [binder, in WiSE.symbolic.symex]
-p1:154 [binder, in WiSE.lang.imp]
-p1:160 [binder, in WiSE.lang.imp]
-p1:166 [binder, in WiSE.lang.imp]
-p1:170 [binder, in WiSE.lang.imp]
-p2:105 [binder, in WiSE.symbolic.symex]
-p2:155 [binder, in WiSE.lang.imp]
-p2:161 [binder, in WiSE.lang.imp]
-p2:167 [binder, in WiSE.lang.imp]
-p2:171 [binder, in WiSE.lang.imp]
-P:100 [binder, in WiSE.streams]
-P:108 [binder, in WiSE.streams]
-p:110 [binder, in WiSE.symbolic.symex]
-P:111 [binder, in WiSE.streams]
-P:115 [binder, in WiSE.streams]
-p:116 [binder, in WiSE.symbolic.symex]
-p:119 [binder, in WiSE.symbolic.symex]
-P:119 [binder, in WiSE.streams]
-p:134 [binder, in WiSE.lang.imp]
-p:137 [binder, in WiSE.symbolic.symex]
-p:138 [binder, in WiSE.symbolic.symex]
-p:142 [binder, in WiSE.lang.imp]
-p:143 [binder, in WiSE.symbolic.symex]
-p:145 [binder, in WiSE.symbolic.symex]
-p:145 [binder, in WiSE.lang.imp]
-p:147 [binder, in WiSE.symbolic.symex]
-p:151 [binder, in WiSE.symbolic.symex]
-p:153 [binder, in WiSE.symbolic.symex]
-p:155 [binder, in WiSE.symbolic.symex]
-p:156 [binder, in WiSE.symbolic.symex]
-p:158 [binder, in WiSE.symbolic.symex]
-p:164 [binder, in WiSE.lang.imp]
-p:173 [binder, in WiSE.lang.imp]
-p:174 [binder, in WiSE.lang.imp]
-p:177 [binder, in WiSE.lang.imp]
-p:178 [binder, in WiSE.lang.imp]
-p:184 [binder, in WiSE.lang.imp]
-p:185 [binder, in WiSE.lang.imp]
-p:189 [binder, in WiSE.lang.imp]
-p:191 [binder, in WiSE.lang.imp]
-p:193 [binder, in WiSE.lang.imp]
-p:197 [binder, in WiSE.lang.imp]
-p:26 [binder, in WiSE.implem.bugfinder]
-p:27 [binder, in WiSE.implem.bugfinder]
-p:28 [binder, in WiSE.implem.bugfinder]
-p:30 [binder, in WiSE.implem.bugfinder]
-p:48 [binder, in WiSE.implem.bugfinder_proof]
-p:5 [binder, in WiSE.implem.bugfinder]
-p:67 [binder, in WiSE.implem.bugfinder_proof]
-P:68 [binder, in WiSE.streams]
-p:68 [binder, in WiSE.implem.bugfinder_proof]
-p:70 [binder, in WiSE.implem.bugfinder_proof]
-P:71 [binder, in WiSE.streams]
-p:73 [binder, in WiSE.implem.bugfinder_proof]
-P:75 [binder, in WiSE.streams]
-P:79 [binder, in WiSE.streams]
-p:79 [binder, in WiSE.implem.bugfinder_proof]
-p:81 [binder, in WiSE.implem.bugfinder_proof]
-p:82 [binder, in WiSE.implem.bugfinder_proof]
-P:83 [binder, in WiSE.streams]
-P:87 [binder, in WiSE.streams]
-P:91 [binder, in WiSE.streams]
-P:94 [binder, in WiSE.streams]
-

Q

-Q:120 [binder, in WiSE.streams]
-q:4 [binder, in WiSE.implem.bugfinder]
-Q:80 [binder, in WiSE.streams]
-Q:84 [binder, in WiSE.streams]
-Q:88 [binder, in WiSE.streams]
-

R

-RA:21 [binder, in WiSE.relations]
-RA:30 [binder, in WiSE.relations]
-RB:22 [binder, in WiSE.relations]
-RB:31 [binder, in WiSE.relations]
-Reach [definition, in WiSE.symbolic.symex]
-Reach [definition, in WiSE.lang.imp]
-reachable_from [definition, in WiSE.implem.bugfinder_proof]
-Reach_complete [lemma, in WiSE.symbolic.symex]
-Reach_sound [lemma, in WiSE.symbolic.symex]
-reduce [definition, in WiSE.utils]
-relations [library]
-relatively_sound_bug_finding [definition, in WiSE.symbolic.symex]
-relative_soundness [lemma, in WiSE.implem.bugfinder_proof]
-relative_completeness [lemma, in WiSE.implem.bugfinder_proof]
-run [definition, in WiSE.implem.bugfinder]
-run_finished [lemma, in WiSE.implem.bugfinder_proof]
-run_finished_nil [lemma, in WiSE.implem.bugfinder_proof]
-run_complete [lemma, in WiSE.implem.bugfinder_proof]
-run_steps_complete [lemma, in WiSE.implem.bugfinder_proof]
-run_here [lemma, in WiSE.implem.bugfinder_proof]
-run_step_complete [lemma, in WiSE.implem.bugfinder_proof]
-run_sound [lemma, in WiSE.implem.bugfinder_proof]
-run_n_S_length [lemma, in WiSE.implem.bugfinder_proof]
-run_n_length [lemma, in WiSE.implem.bugfinder_proof]
-run_n_nil [lemma, in WiSE.implem.bugfinder_proof]
-run_run_n [lemma, in WiSE.implem.bugfinder_proof]
-run_nil [lemma, in WiSE.implem.bugfinder_proof]
-run_eq [lemma, in WiSE.implem.bugfinder_proof]
-run_n [definition, in WiSE.implem.bugfinder]
-

S

-SAT [constructor, in WiSE.symbolic.solver]
-sat [inductive, in WiSE.symbolic.solver]
-scons [constructor, in WiSE.streams]
-senv1:63 [binder, in WiSE.symbolic.symex]
-senv1:71 [binder, in WiSE.symbolic.symex]
-senv1:80 [binder, in WiSE.symbolic.symex]
-senv1:88 [binder, in WiSE.symbolic.symex]
-senv1:95 [binder, in WiSE.symbolic.symex]
-senv2:64 [binder, in WiSE.symbolic.symex]
-senv2:74 [binder, in WiSE.symbolic.symex]
-senv2:83 [binder, in WiSE.symbolic.symex]
-senv2:89 [binder, in WiSE.symbolic.symex]
-senv2:96 [binder, in WiSE.symbolic.symex]
-senv:103 [binder, in WiSE.symbolic.symex]
-senv:111 [binder, in WiSE.symbolic.symex]
-senv:127 [binder, in WiSE.symbolic.symex]
-senv:135 [binder, in WiSE.symbolic.symex]
-senv:19 [binder, in WiSE.symbolic.symex]
-senv:22 [binder, in WiSE.symbolic.symex]
-senv:25 [binder, in WiSE.symbolic.symex]
-Seq [constructor, in WiSE.lang.imprec]
-Seq [constructor, in WiSE.lang.imp]
-Sequences [section, in WiSE.relations]
-Sequences.A [variable, in WiSE.relations]
-Sequences.R [variable, in WiSE.relations]
-shift [definition, in WiSE.streams]
-shift_eq [lemma, in WiSE.streams]
-sim [definition, in WiSE.symbolic.symex]
-simulation [definition, in WiSE.relations]
-Simulation [section, in WiSE.relations]
-sim_init [lemma, in WiSE.symbolic.symex]
-sim:23 [binder, in WiSE.relations]
-sim:32 [binder, in WiSE.relations]
-Skip [constructor, in WiSE.lang.imprec]
-Skip [constructor, in WiSE.lang.imp]
-solver [definition, in WiSE.symbolic.solver]
-solver [library]
-solver_correct [lemma, in WiSE.symbolic.solver]
-sound_termination [lemma, in WiSE.implem.bugfinder_proof]
-star [inductive, in WiSE.relations]
-starr [inductive, in WiSE.relations]
-starr_star [lemma, in WiSE.relations]
-starr_reflexive [instance, in WiSE.relations]
-starr_trans [instance, in WiSE.relations]
-starr_step [constructor, in WiSE.relations]
-starr_refl [constructor, in WiSE.relations]
-star_simulation [lemma, in WiSE.relations]
-star_trans [instance, in WiSE.relations]
-star_reflexive [instance, in WiSE.relations]
-star_one [lemma, in WiSE.relations]
-star_step [constructor, in WiSE.relations]
-star_refl [constructor, in WiSE.relations]
-status [inductive, in WiSE.implem.bugfinder]
-step [inductive, in WiSE.lang.imp]
-steps [definition, in WiSE.lang.imp]
-steps_simulation_diagram [lemma, in WiSE.symbolic.symex]
-steps_exec [lemma, in WiSE.lang.imp]
-steps_seq [lemma, in WiSE.lang.imp]
-step_simulation_diagram [lemma, in WiSE.symbolic.symex]
-step_exec_exec [lemma, in WiSE.lang.imp]
-step_Loop_false [constructor, in WiSE.lang.imp]
-step_Loop_true [constructor, in WiSE.lang.imp]
-step_Ite_false [constructor, in WiSE.lang.imp]
-step_Ite_true [constructor, in WiSE.lang.imp]
-step_Seq_Skip [constructor, in WiSE.lang.imp]
-step_Seq [constructor, in WiSE.lang.imp]
-step_Aff [constructor, in WiSE.lang.imp]
-stmt [inductive, in WiSE.lang.imprec]
-store [definition, in WiSE.lang.imp]
-stream [inductive, in WiSE.streams]
-streams [library]
-stream_func_iso [lemma, in WiSE.streams]
-stream_Eq [instance, in WiSE.streams]
-stream_equ [definition, in WiSE.streams]
-str:101 [binder, in WiSE.streams]
-str:65 [binder, in WiSE.streams]
-Stuck [definition, in WiSE.lang.imp]
-st:150 [binder, in WiSE.lang.imp]
-st:24 [binder, in WiSE.implem.bugfinder]
-st:43 [binder, in WiSE.implem.bugfinder_proof]
-st:46 [binder, in WiSE.implem.bugfinder_proof]
-st:49 [binder, in WiSE.implem.bugfinder_proof]
-st:51 [binder, in WiSE.implem.bugfinder_proof]
-st:53 [binder, in WiSE.implem.bugfinder_proof]
-st:74 [binder, in WiSE.implem.bugfinder_proof]
-st:77 [binder, in WiSE.implem.bugfinder_proof]
-Sub [constructor, in WiSE.lang.imprec]
-Sub [constructor, in WiSE.lang.imp]
-Symbolic [definition, in WiSE.implem.bugfinder_proof]
-symex [library]
-symex_complete [lemma, in WiSE.symbolic.symex]
-symex_sound [lemma, in WiSE.symbolic.symex]
-sym_steps_steps [lemma, in WiSE.symbolic.symex]
-sym_steps_steps_aux [lemma, in WiSE.symbolic.symex]
-sym_steps_path [lemma, in WiSE.symbolic.symex]
-sym_step_path [lemma, in WiSE.symbolic.symex]
-sym_step_step [lemma, in WiSE.symbolic.symex]
-sym_steps [definition, in WiSE.symbolic.symex]
-sym_step_Loop_false [constructor, in WiSE.symbolic.symex]
-sym_step_Loop_true [constructor, in WiSE.symbolic.symex]
-sym_step_Ite_false [constructor, in WiSE.symbolic.symex]
-sym_step_Ite_true [constructor, in WiSE.symbolic.symex]
-sym_step_Seq_Skip [constructor, in WiSE.symbolic.symex]
-sym_step_Seq [constructor, in WiSE.symbolic.symex]
-sym_step_Aff [constructor, in WiSE.symbolic.symex]
-sym_step [inductive, in WiSE.symbolic.symex]
-sym_state [definition, in WiSE.symbolic.symex]
-sym_beval [definition, in WiSE.symbolic.symex]
-sym_aeval [definition, in WiSE.symbolic.symex]
-sym_update [definition, in WiSE.symbolic.symex]
-sym_store [definition, in WiSE.symbolic.symex]
-s'':77 [binder, in WiSE.lang.imp]
-s'':92 [binder, in WiSE.lang.imp]
-s':121 [binder, in WiSE.symbolic.symex]
-s':123 [binder, in WiSE.symbolic.symex]
-s':136 [binder, in WiSE.lang.imp]
-s':144 [binder, in WiSE.lang.imp]
-s':148 [binder, in WiSE.lang.imp]
-s':181 [binder, in WiSE.lang.imp]
-s':58 [binder, in WiSE.implem.bugfinder_proof]
-s':61 [binder, in WiSE.implem.bugfinder_proof]
-s':64 [binder, in WiSE.implem.bugfinder_proof]
-s':69 [binder, in WiSE.implem.bugfinder_proof]
-s':76 [binder, in WiSE.lang.imp]
-s':81 [binder, in WiSE.lang.imp]
-s':86 [binder, in WiSE.lang.imp]
-s':91 [binder, in WiSE.lang.imp]
-s0:41 [binder, in WiSE.implem.bugfinder_proof]
-s1:104 [binder, in WiSE.lang.imp]
-s1:125 [binder, in WiSE.streams]
-s1:129 [binder, in WiSE.lang.imp]
-s1:139 [binder, in WiSE.lang.imp]
-s1:19 [binder, in WiSE.implem.bugfinder_proof]
-s1:37 [binder, in WiSE.symbolic.symex]
-s2:105 [binder, in WiSE.lang.imp]
-s2:126 [binder, in WiSE.streams]
-s2:130 [binder, in WiSE.lang.imp]
-s2:140 [binder, in WiSE.lang.imp]
-s2:20 [binder, in WiSE.implem.bugfinder_proof]
-s2:38 [binder, in WiSE.symbolic.symex]
-s3:141 [binder, in WiSE.lang.imp]
-s:10 [binder, in WiSE.symbolic.symex]
-s:10 [binder, in WiSE.streams]
-s:100 [binder, in WiSE.lang.imp]
-s:104 [binder, in WiSE.streams]
-s:107 [binder, in WiSE.streams]
-s:109 [binder, in WiSE.lang.imp]
-s:110 [binder, in WiSE.streams]
-s:111 [binder, in WiSE.lang.imp]
-s:114 [binder, in WiSE.streams]
-s:115 [binder, in WiSE.lang.imp]
-s:118 [binder, in WiSE.streams]
-s:119 [binder, in WiSE.lang.imp]
-s:120 [binder, in WiSE.symbolic.symex]
-s:122 [binder, in WiSE.symbolic.symex]
-s:122 [binder, in WiSE.lang.imp]
-s:13 [binder, in WiSE.streams]
-s:135 [binder, in WiSE.lang.imp]
-s:14 [binder, in WiSE.symbolic.symex]
-s:143 [binder, in WiSE.lang.imp]
-s:146 [binder, in WiSE.lang.imp]
-s:165 [binder, in WiSE.lang.imp]
-s:172 [binder, in WiSE.lang.imp]
-s:18 [binder, in WiSE.implem.bugfinder_proof]
-s:180 [binder, in WiSE.lang.imp]
-s:19 [binder, in WiSE.streams]
-s:2 [binder, in WiSE.symbolic.symex]
-s:22 [binder, in WiSE.lang.imprec]
-s:24 [binder, in WiSE.streams]
-s:24 [binder, in WiSE.lang.imp]
-s:3 [binder, in WiSE.implem.bugfinder]
-s:30 [binder, in WiSE.symbolic.symex]
-s:33 [binder, in WiSE.streams]
-s:36 [binder, in WiSE.implem.bugfinder]
-s:36 [binder, in WiSE.lang.imp]
-s:39 [binder, in WiSE.implem.bugfinder_proof]
-s:40 [binder, in WiSE.streams]
-s:42 [binder, in WiSE.symbolic.symex]
-s:42 [binder, in WiSE.implem.bugfinder_proof]
-s:45 [binder, in WiSE.symbolic.symex]
-s:45 [binder, in WiSE.implem.bugfinder_proof]
-s:48 [binder, in WiSE.lang.imp]
-s:50 [binder, in WiSE.symbolic.symex]
-s:50 [binder, in WiSE.streams]
-s:52 [binder, in WiSE.lang.imp]
-s:55 [binder, in WiSE.symbolic.symex]
-s:55 [binder, in WiSE.streams]
-s:56 [binder, in WiSE.lang.imp]
-s:57 [binder, in WiSE.implem.bugfinder_proof]
-s:59 [binder, in WiSE.symbolic.symex]
-s:59 [binder, in WiSE.implem.bugfinder_proof]
-s:60 [binder, in WiSE.implem.bugfinder_proof]
-s:60 [binder, in WiSE.lang.imp]
-s:61 [binder, in WiSE.streams]
-s:63 [binder, in WiSE.implem.bugfinder_proof]
-s:64 [binder, in WiSE.lang.imp]
-s:69 [binder, in WiSE.streams]
-s:7 [binder, in WiSE.symbolic.symex]
-s:7 [binder, in WiSE.streams]
-s:70 [binder, in WiSE.lang.imp]
-s:71 [binder, in WiSE.lang.imp]
-s:72 [binder, in WiSE.streams]
-s:75 [binder, in WiSE.lang.imp]
-s:76 [binder, in WiSE.streams]
-s:80 [binder, in WiSE.lang.imp]
-s:81 [binder, in WiSE.streams]
-s:85 [binder, in WiSE.streams]
-s:85 [binder, in WiSE.lang.imp]
-s:89 [binder, in WiSE.streams]
-s:90 [binder, in WiSE.lang.imp]
-s:92 [binder, in WiSE.streams]
-s:95 [binder, in WiSE.streams]
-s:95 [binder, in WiSE.lang.imp]
-

T

-tasks [definition, in WiSE.implem.bugfinder]
-tasks:19 [binder, in WiSE.implem.bugfinder]
-tasks:38 [binder, in WiSE.implem.bugfinder_proof]
-then_do [definition, in WiSE.implem.bugfinder]
-trivial_assertion [definition, in WiSE.implem.bugfinder]
-t:10 [binder, in WiSE.implem.bugfinder_proof]
-t:14 [binder, in WiSE.implem.bugfinder_proof]
-

U

-UNSAT [constructor, in WiSE.symbolic.solver]
-untill [definition, in WiSE.streams]
-update [definition, in WiSE.lang.imp]
-utils [library]
-

V

-ValidBug [definition, in WiSE.implem.bugfinder_proof]
-ValidStatus [definition, in WiSE.implem.bugfinder_proof]
-Var [constructor, in WiSE.lang.imprec]
-Var [constructor, in WiSE.lang.imp]
-variable [inductive, in WiSE.lang.imprec]
-ve:103 [binder, in WiSE.lang.imp]
-ve:34 [binder, in WiSE.symbolic.symex]
-ve:74 [binder, in WiSE.lang.imp]
-vx:35 [binder, in WiSE.lang.imp]
-vx:47 [binder, in WiSE.lang.imp]
-vx:63 [binder, in WiSE.lang.imp]
-vx:67 [binder, in WiSE.lang.imp]
-V0:141 [binder, in WiSE.symbolic.symex]
-V0:148 [binder, in WiSE.symbolic.symex]
-V0:159 [binder, in WiSE.symbolic.symex]
-V0:163 [binder, in WiSE.symbolic.symex]
-V0:188 [binder, in WiSE.lang.imp]
-V0:194 [binder, in WiSE.lang.imp]
-V:196 [binder, in WiSE.lang.imp]
-v:50 [binder, in WiSE.lang.imp]
-

X

-xs:13 [binder, in WiSE.utils]
-xs:18 [binder, in WiSE.utils]
-xs:30 [binder, in WiSE.streams]
-xs:47 [binder, in WiSE.streams]
-xs:5 [binder, in WiSE.streams]
-x:1 [binder, in WiSE.symbolic.symex]
-x:101 [binder, in WiSE.lang.imp]
-x:102 [binder, in WiSE.streams]
-x:128 [binder, in WiSE.lang.imp]
-x:13 [binder, in WiSE.relations]
-x:14 [binder, in WiSE.relations]
-x:143 [binder, in WiSE.streams]
-x:145 [binder, in WiSE.streams]
-x:15 [binder, in WiSE.lang.imprec]
-x:157 [binder, in WiSE.lang.imp]
-x:17 [binder, in WiSE.relations]
-x:19 [binder, in WiSE.lang.imprec]
-x:23 [binder, in WiSE.lang.imprec]
-x:27 [binder, in WiSE.symbolic.symex]
-x:29 [binder, in WiSE.lang.imprec]
-x:29 [binder, in WiSE.streams]
-x:29 [binder, in WiSE.lang.imp]
-x:3 [binder, in WiSE.lang.imprec]
-x:3 [binder, in WiSE.symbolic.symex]
-x:32 [binder, in WiSE.symbolic.symex]
-x:32 [binder, in WiSE.implem.bugfinder]
-x:34 [binder, in WiSE.implem.bugfinder]
-x:34 [binder, in WiSE.lang.imp]
-x:4 [binder, in WiSE.lang.imprec]
-x:4 [binder, in WiSE.streams]
-x:41 [binder, in WiSE.lang.imp]
-x:46 [binder, in WiSE.streams]
-x:46 [binder, in WiSE.lang.imp]
-x:49 [binder, in WiSE.lang.imp]
-x:5 [binder, in WiSE.relations]
-x:54 [binder, in WiSE.lang.imp]
-x:58 [binder, in WiSE.lang.imp]
-x:6 [binder, in WiSE.relations]
-x:62 [binder, in WiSE.lang.imp]
-x:66 [binder, in WiSE.lang.imp]
-x:72 [binder, in WiSE.lang.imp]
-X:77 [binder, in WiSE.symbolic.symex]
-x:8 [binder, in WiSE.symbolic.symex]
-X:86 [binder, in WiSE.symbolic.symex]
-x:9 [binder, in WiSE.relations]
-x:96 [binder, in WiSE.streams]
-

Y

-y:10 [binder, in WiSE.relations]
-y:15 [binder, in WiSE.relations]
-y:18 [binder, in WiSE.relations]
-y:5 [binder, in WiSE.symbolic.symex]
-y:51 [binder, in WiSE.lang.imp]
-y:6 [binder, in WiSE.utils]
-y:7 [binder, in WiSE.relations]
-Y:78 [binder, in WiSE.symbolic.symex]
-Y:87 [binder, in WiSE.symbolic.symex]
-

Z

-z:16 [binder, in WiSE.relations]
-z:8 [binder, in WiSE.relations]
-

other

-_ @ _ ≃ _ [notation, in WiSE.symbolic.symex]
-_ ∘ _ [notation, in WiSE.symbolic.symex]
-_ ≃ _ [notation, in WiSE.equalities]
-_ ≡ _ [notation, in WiSE.equalities]
-!! _ [notation, in WiSE.implem.bugfinder_proof]
-! _ [notation, in WiSE.implem.bugfinder_proof]
-π1:35 [binder, in WiSE.symbolic.symex]
-π1:65 [binder, in WiSE.symbolic.symex]
-π1:70 [binder, in WiSE.symbolic.symex]
-π1:79 [binder, in WiSE.symbolic.symex]
-π1:90 [binder, in WiSE.symbolic.symex]
-π1:97 [binder, in WiSE.symbolic.symex]
-π2:36 [binder, in WiSE.symbolic.symex]
-π2:66 [binder, in WiSE.symbolic.symex]
-π2:73 [binder, in WiSE.symbolic.symex]
-π2:82 [binder, in WiSE.symbolic.symex]
-π2:91 [binder, in WiSE.symbolic.symex]
-π2:98 [binder, in WiSE.symbolic.symex]
-π:101 [binder, in WiSE.symbolic.symex]
-π:112 [binder, in WiSE.symbolic.symex]
-π:134 [binder, in WiSE.symbolic.symex]
-π:31 [binder, in WiSE.symbolic.symex]
-π:44 [binder, in WiSE.symbolic.symex]
-π:49 [binder, in WiSE.symbolic.symex]
-π:54 [binder, in WiSE.symbolic.symex]
-π:58 [binder, in WiSE.symbolic.symex]
-σ':142 [binder, in WiSE.symbolic.symex]
-σ':150 [binder, in WiSE.symbolic.symex]
-σ':162 [binder, in WiSE.symbolic.symex]
-σ':71 [binder, in WiSE.implem.bugfinder_proof]
-σ:139 [binder, in WiSE.symbolic.symex]
-σ:140 [binder, in WiSE.symbolic.symex]
-σ:144 [binder, in WiSE.symbolic.symex]
-σ:146 [binder, in WiSE.symbolic.symex]
-σ:149 [binder, in WiSE.symbolic.symex]
-σ:152 [binder, in WiSE.symbolic.symex]
-σ:154 [binder, in WiSE.symbolic.symex]
-σ:157 [binder, in WiSE.symbolic.symex]
-σ:160 [binder, in WiSE.symbolic.symex]
-σ:161 [binder, in WiSE.symbolic.symex]
-σ:183 [binder, in WiSE.lang.imp]
-σ:186 [binder, in WiSE.lang.imp]
-σ:187 [binder, in WiSE.lang.imp]
-σ:190 [binder, in WiSE.lang.imp]
-σ:192 [binder, in WiSE.lang.imp]
-σ:195 [binder, in WiSE.lang.imp]
-σ:72 [binder, in WiSE.implem.bugfinder_proof]
-σ:76 [binder, in WiSE.implem.bugfinder_proof]
-σ:80 [binder, in WiSE.implem.bugfinder_proof]
-

-

Notation Index

-

E

-Bug _ [in WiSE.implem.bugfinder]
-

L

-_ ⊨ _ [in WiSE.streams]
-_ ∧ _ [in WiSE.streams]
-_ ∨ _ [in WiSE.streams]
-_ → _ [in WiSE.streams]
-!! _ [in WiSE.streams]
-! _ [in WiSE.streams]
-¬ _ [in WiSE.streams]
-□ _ [in WiSE.streams]
-◊ _ [in WiSE.streams]
-◯ _ [in WiSE.streams]
-

other

-_ @ _ ≃ _ [in WiSE.symbolic.symex]
-_ ∘ _ [in WiSE.symbolic.symex]
-_ ≃ _ [in WiSE.equalities]
-_ ≡ _ [in WiSE.equalities]
-!! _ [in WiSE.implem.bugfinder_proof]
-! _ [in WiSE.implem.bugfinder_proof]
-

-

Binder Index

-

A

-a1:1 [in WiSE.symbolic.solver]
-a1:13 [in WiSE.symbolic.solver]
-a1:16 [in WiSE.symbolic.solver]
-a1:24 [in WiSE.relations]
-a1:3 [in WiSE.lang.imp]
-a1:5 [in WiSE.symbolic.solver]
-a2:14 [in WiSE.symbolic.solver]
-a2:17 [in WiSE.symbolic.solver]
-a2:2 [in WiSE.symbolic.solver]
-a2:25 [in WiSE.relations]
-a2:4 [in WiSE.lang.imp]
-a2:6 [in WiSE.symbolic.solver]
-A:1 [in WiSE.streams]
-A:1 [in WiSE.equalities]
-A:1 [in WiSE.utils]
-A:1 [in WiSE.implem.bugfinder_proof]
-a:10 [in WiSE.equalities]
-A:103 [in WiSE.streams]
-A:106 [in WiSE.streams]
-A:109 [in WiSE.streams]
-A:11 [in WiSE.streams]
-A:113 [in WiSE.streams]
-A:117 [in WiSE.streams]
-A:12 [in WiSE.equalities]
-A:123 [in WiSE.streams]
-A:124 [in WiSE.streams]
-A:128 [in WiSE.streams]
-A:132 [in WiSE.streams]
-A:133 [in WiSE.streams]
-A:134 [in WiSE.streams]
-A:138 [in WiSE.streams]
-A:14 [in WiSE.utils]
-A:142 [in WiSE.streams]
-A:17 [in WiSE.streams]
-a:19 [in WiSE.symbolic.solver]
-A:19 [in WiSE.utils]
-A:19 [in WiSE.relations]
-a:19 [in WiSE.lang.imp]
-A:23 [in WiSE.streams]
-A:27 [in WiSE.streams]
-A:28 [in WiSE.relations]
-A:31 [in WiSE.streams]
-A:37 [in WiSE.streams]
-A:4 [in WiSE.equalities]
-A:43 [in WiSE.streams]
-A:48 [in WiSE.streams]
-A:53 [in WiSE.streams]
-A:58 [in WiSE.streams]
-A:6 [in WiSE.streams]
-a:6 [in WiSE.implem.bugfinder_proof]
-A:62 [in WiSE.streams]
-A:66 [in WiSE.streams]
-A:67 [in WiSE.streams]
-A:7 [in WiSE.utils]
-A:70 [in WiSE.streams]
-A:74 [in WiSE.streams]
-A:78 [in WiSE.streams]
-a:8 [in WiSE.lang.imp]
-A:82 [in WiSE.streams]
-A:86 [in WiSE.streams]
-a:9 [in WiSE.symbolic.solver]
-A:9 [in WiSE.streams]
-A:90 [in WiSE.streams]
-A:93 [in WiSE.streams]
-A:97 [in WiSE.streams]
-

B

-b1:12 [in WiSE.lang.imp]
-b1:14 [in WiSE.lang.imp]
-b1:20 [in WiSE.symbolic.solver]
-b1:26 [in WiSE.relations]
-b1:30 [in WiSE.symbolic.solver]
-b1:9 [in WiSE.lang.imprec]
-b2:10 [in WiSE.lang.imprec]
-b2:13 [in WiSE.lang.imp]
-b2:15 [in WiSE.lang.imp]
-b2:21 [in WiSE.symbolic.solver]
-b2:27 [in WiSE.relations]
-b2:31 [in WiSE.symbolic.solver]
-b:11 [in WiSE.equalities]
-B:13 [in WiSE.equalities]
-b:153 [in WiSE.lang.imp]
-b:163 [in WiSE.lang.imp]
-b:18 [in WiSE.lang.imprec]
-B:2 [in WiSE.implem.bugfinder_proof]
-B:20 [in WiSE.relations]
-b:20 [in WiSE.lang.imp]
-b:24 [in WiSE.symbolic.solver]
-b:26 [in WiSE.symbolic.solver]
-B:29 [in WiSE.relations]
-b:33 [in WiSE.symbolic.solver]
-b:35 [in WiSE.symbolic.solver]
-b:38 [in WiSE.symbolic.solver]
-B:38 [in WiSE.streams]
-b:39 [in WiSE.symbolic.solver]
-b:42 [in WiSE.symbolic.solver]
-B:44 [in WiSE.streams]
-B:5 [in WiSE.equalities]
-b:5 [in WiSE.implem.bugfinder_proof]
-B:59 [in WiSE.streams]
-B:8 [in WiSE.utils]
-b:9 [in WiSE.lang.imp]
-B:98 [in WiSE.streams]
-

C

-cond:29 [in WiSE.implem.bugfinder]
-cond:31 [in WiSE.implem.bugfinder]
-c1:106 [in WiSE.lang.imp]
-c1:113 [in WiSE.lang.imp]
-c1:117 [in WiSE.lang.imp]
-c1:131 [in WiSE.lang.imp]
-c1:137 [in WiSE.lang.imp]
-c1:39 [in WiSE.symbolic.symex]
-c1:47 [in WiSE.symbolic.symex]
-c1:52 [in WiSE.symbolic.symex]
-c1:67 [in WiSE.symbolic.symex]
-c1:72 [in WiSE.symbolic.symex]
-c1:78 [in WiSE.lang.imp]
-c1:81 [in WiSE.symbolic.symex]
-c1:83 [in WiSE.lang.imp]
-c1:88 [in WiSE.lang.imp]
-c1:92 [in WiSE.symbolic.symex]
-c1:99 [in WiSE.symbolic.symex]
-c2:100 [in WiSE.symbolic.symex]
-c2:107 [in WiSE.lang.imp]
-c2:114 [in WiSE.lang.imp]
-c2:118 [in WiSE.lang.imp]
-c2:132 [in WiSE.lang.imp]
-c2:138 [in WiSE.lang.imp]
-c2:40 [in WiSE.symbolic.symex]
-c2:48 [in WiSE.symbolic.symex]
-c2:53 [in WiSE.symbolic.symex]
-c2:68 [in WiSE.symbolic.symex]
-c2:75 [in WiSE.symbolic.symex]
-c2:79 [in WiSE.lang.imp]
-c2:84 [in WiSE.symbolic.symex]
-c2:84 [in WiSE.lang.imp]
-c2:89 [in WiSE.lang.imp]
-c2:93 [in WiSE.symbolic.symex]
-c3:108 [in WiSE.lang.imp]
-c3:133 [in WiSE.lang.imp]
-c3:41 [in WiSE.symbolic.symex]
-c:110 [in WiSE.lang.imp]
-c:121 [in WiSE.lang.imp]
-c:124 [in WiSE.lang.imp]
-c:13 [in WiSE.lang.imprec]
-c:23 [in WiSE.lang.imp]
-c:43 [in WiSE.symbolic.symex]
-c:57 [in WiSE.symbolic.symex]
-c:57 [in WiSE.lang.imp]
-c:61 [in WiSE.symbolic.symex]
-c:65 [in WiSE.lang.imp]
-c:94 [in WiSE.lang.imp]
-c:97 [in WiSE.lang.imp]
-

E

-env0:106 [in WiSE.symbolic.symex]
-env0:114 [in WiSE.symbolic.symex]
-env0:117 [in WiSE.symbolic.symex]
-env0:129 [in WiSE.symbolic.symex]
-env0:130 [in WiSE.symbolic.symex]
-env1:125 [in WiSE.lang.imp]
-env1:132 [in WiSE.symbolic.symex]
-env2:126 [in WiSE.lang.imp]
-env:10 [in WiSE.implem.bugfinder]
-env:102 [in WiSE.symbolic.symex]
-env:108 [in WiSE.symbolic.symex]
-env:115 [in WiSE.symbolic.symex]
-env:118 [in WiSE.symbolic.symex]
-env:12 [in WiSE.symbolic.solver]
-env:12 [in WiSE.implem.bugfinder_proof]
-env:15 [in WiSE.symbolic.solver]
-env:151 [in WiSE.lang.imp]
-env:152 [in WiSE.lang.imp]
-env:156 [in WiSE.lang.imp]
-env:159 [in WiSE.lang.imp]
-env:16 [in WiSE.implem.bugfinder_proof]
-env:162 [in WiSE.lang.imp]
-env:18 [in WiSE.symbolic.symex]
-env:18 [in WiSE.symbolic.solver]
-env:21 [in WiSE.symbolic.symex]
-env:23 [in WiSE.implem.bugfinder_proof]
-env:24 [in WiSE.symbolic.symex]
-env:29 [in WiSE.symbolic.solver]
-env:32 [in WiSE.symbolic.solver]
-env:34 [in WiSE.symbolic.solver]
-env:35 [in WiSE.implem.bugfinder_proof]
-env:40 [in WiSE.symbolic.solver]
-env:41 [in WiSE.symbolic.solver]
-env:6 [in WiSE.symbolic.symex]
-env:6 [in WiSE.implem.bugfinder]
-env:62 [in WiSE.symbolic.symex]
-env:69 [in WiSE.symbolic.symex]
-env:76 [in WiSE.symbolic.symex]
-env:8 [in WiSE.implem.bugfinder_proof]
-env:85 [in WiSE.symbolic.symex]
-env:9 [in WiSE.symbolic.symex]
-env:94 [in WiSE.symbolic.symex]
-e':30 [in WiSE.lang.imp]
-e':42 [in WiSE.lang.imp]
-e':55 [in WiSE.lang.imp]
-e:102 [in WiSE.lang.imp]
-e:11 [in WiSE.symbolic.symex]
-e:112 [in WiSE.lang.imp]
-e:116 [in WiSE.lang.imp]
-e:120 [in WiSE.lang.imp]
-e:123 [in WiSE.lang.imp]
-e:127 [in WiSE.lang.imp]
-e:14 [in WiSE.lang.imprec]
-e:15 [in WiSE.symbolic.symex]
-e:158 [in WiSE.lang.imp]
-e:20 [in WiSE.symbolic.symex]
-e:23 [in WiSE.symbolic.symex]
-e:25 [in WiSE.lang.imp]
-e:26 [in WiSE.symbolic.symex]
-e:28 [in WiSE.lang.imp]
-e:33 [in WiSE.symbolic.symex]
-e:33 [in WiSE.lang.imp]
-e:36 [in WiSE.lang.imprec]
-e:37 [in WiSE.lang.imp]
-e:4 [in WiSE.symbolic.symex]
-e:40 [in WiSE.lang.imp]
-e:45 [in WiSE.lang.imp]
-e:46 [in WiSE.symbolic.symex]
-e:51 [in WiSE.symbolic.symex]
-e:53 [in WiSE.lang.imp]
-e:56 [in WiSE.symbolic.symex]
-e:59 [in WiSE.lang.imp]
-e:60 [in WiSE.symbolic.symex]
-e:61 [in WiSE.lang.imp]
-e:73 [in WiSE.lang.imp]
-e:82 [in WiSE.lang.imp]
-e:87 [in WiSE.lang.imp]
-e:93 [in WiSE.lang.imp]
-e:96 [in WiSE.lang.imp]
-

F

-f1:129 [in WiSE.streams]
-f2:130 [in WiSE.streams]
-f:105 [in WiSE.streams]
-f:136 [in WiSE.streams]
-f:140 [in WiSE.streams]
-f:16 [in WiSE.equalities]
-f:2 [in WiSE.utils]
-f:3 [in WiSE.implem.bugfinder_proof]
-f:39 [in WiSE.streams]
-f:45 [in WiSE.streams]
-f:49 [in WiSE.streams]
-f:54 [in WiSE.streams]
-f:60 [in WiSE.streams]
-f:8 [in WiSE.equalities]
-f:9 [in WiSE.utils]
-f:99 [in WiSE.streams]
-

G

-gs:34 [in WiSE.lang.imprec]
-g:17 [in WiSE.equalities]
-g:9 [in WiSE.equalities]
-

H

-H0:15 [in WiSE.equalities]
-H0:7 [in WiSE.equalities]
-H:14 [in WiSE.equalities]
-H:6 [in WiSE.equalities]
-

L

-ls:35 [in WiSE.lang.imprec]
-l1:29 [in WiSE.implem.bugfinder_proof]
-l1:32 [in WiSE.implem.bugfinder_proof]
-l2:30 [in WiSE.implem.bugfinder_proof]
-l2:33 [in WiSE.implem.bugfinder_proof]
-l3:31 [in WiSE.implem.bugfinder_proof]
-l3:37 [in WiSE.implem.bugfinder_proof]
-l:10 [in WiSE.utils]
-l:14 [in WiSE.implem.bugfinder]
-l:15 [in WiSE.utils]
-l:20 [in WiSE.utils]
-l:21 [in WiSE.implem.bugfinder_proof]
-l:27 [in WiSE.implem.bugfinder_proof]
-l:3 [in WiSE.utils]
-l:4 [in WiSE.implem.bugfinder_proof]
-l:55 [in WiSE.implem.bugfinder_proof]
-l:56 [in WiSE.implem.bugfinder_proof]
-l:62 [in WiSE.implem.bugfinder_proof]
-l:65 [in WiSE.implem.bugfinder_proof]
-l:66 [in WiSE.implem.bugfinder_proof]
-

M

-m:122 [in WiSE.streams]
-m:141 [in WiSE.streams]
-m:26 [in WiSE.streams]
-m:63 [in WiSE.streams]
-

N

-next_next:23 [in WiSE.implem.bugfinder]
-next_next:17 [in WiSE.implem.bugfinder]
-n:112 [in WiSE.streams]
-n:116 [in WiSE.streams]
-n:12 [in WiSE.streams]
-n:121 [in WiSE.streams]
-n:127 [in WiSE.streams]
-n:131 [in WiSE.streams]
-n:135 [in WiSE.streams]
-n:139 [in WiSE.streams]
-n:144 [in WiSE.streams]
-n:146 [in WiSE.streams]
-n:18 [in WiSE.streams]
-n:18 [in WiSE.implem.bugfinder]
-n:25 [in WiSE.streams]
-n:25 [in WiSE.implem.bugfinder_proof]
-n:26 [in WiSE.implem.bugfinder_proof]
-n:28 [in WiSE.streams]
-n:28 [in WiSE.implem.bugfinder_proof]
-n:32 [in WiSE.streams]
-n:56 [in WiSE.streams]
-n:57 [in WiSE.streams]
-n:64 [in WiSE.streams]
-n:73 [in WiSE.streams]
-n:77 [in WiSE.streams]
-

P

-path:11 [in WiSE.implem.bugfinder_proof]
-path:126 [in WiSE.symbolic.symex]
-path:15 [in WiSE.implem.bugfinder_proof]
-path:22 [in WiSE.implem.bugfinder_proof]
-path:34 [in WiSE.implem.bugfinder_proof]
-path:7 [in WiSE.implem.bugfinder_proof]
-path:7 [in WiSE.implem.bugfinder]
-path:9 [in WiSE.implem.bugfinder]
-pat:109 [in WiSE.symbolic.symex]
-pat:113 [in WiSE.symbolic.symex]
-pat:147 [in WiSE.lang.imp]
-pat:8 [in WiSE.implem.bugfinder]
-prog0:125 [in WiSE.symbolic.symex]
-prog0:131 [in WiSE.symbolic.symex]
-prog1:133 [in WiSE.symbolic.symex]
-prog:11 [in WiSE.implem.bugfinder]
-prog:128 [in WiSE.symbolic.symex]
-prog:13 [in WiSE.implem.bugfinder_proof]
-prog:136 [in WiSE.symbolic.symex]
-prog:17 [in WiSE.implem.bugfinder_proof]
-prog:24 [in WiSE.implem.bugfinder_proof]
-prog:36 [in WiSE.implem.bugfinder_proof]
-prog:9 [in WiSE.implem.bugfinder_proof]
-p':107 [in WiSE.symbolic.symex]
-p':149 [in WiSE.lang.imp]
-p1:104 [in WiSE.symbolic.symex]
-p1:154 [in WiSE.lang.imp]
-p1:160 [in WiSE.lang.imp]
-p1:166 [in WiSE.lang.imp]
-p1:170 [in WiSE.lang.imp]
-p2:105 [in WiSE.symbolic.symex]
-p2:155 [in WiSE.lang.imp]
-p2:161 [in WiSE.lang.imp]
-p2:167 [in WiSE.lang.imp]
-p2:171 [in WiSE.lang.imp]
-P:100 [in WiSE.streams]
-P:108 [in WiSE.streams]
-p:110 [in WiSE.symbolic.symex]
-P:111 [in WiSE.streams]
-P:115 [in WiSE.streams]
-p:116 [in WiSE.symbolic.symex]
-p:119 [in WiSE.symbolic.symex]
-P:119 [in WiSE.streams]
-p:134 [in WiSE.lang.imp]
-p:137 [in WiSE.symbolic.symex]
-p:138 [in WiSE.symbolic.symex]
-p:142 [in WiSE.lang.imp]
-p:143 [in WiSE.symbolic.symex]
-p:145 [in WiSE.symbolic.symex]
-p:145 [in WiSE.lang.imp]
-p:147 [in WiSE.symbolic.symex]
-p:151 [in WiSE.symbolic.symex]
-p:153 [in WiSE.symbolic.symex]
-p:155 [in WiSE.symbolic.symex]
-p:156 [in WiSE.symbolic.symex]
-p:158 [in WiSE.symbolic.symex]
-p:164 [in WiSE.lang.imp]
-p:173 [in WiSE.lang.imp]
-p:174 [in WiSE.lang.imp]
-p:177 [in WiSE.lang.imp]
-p:178 [in WiSE.lang.imp]
-p:184 [in WiSE.lang.imp]
-p:185 [in WiSE.lang.imp]
-p:189 [in WiSE.lang.imp]
-p:191 [in WiSE.lang.imp]
-p:193 [in WiSE.lang.imp]
-p:197 [in WiSE.lang.imp]
-p:26 [in WiSE.implem.bugfinder]
-p:27 [in WiSE.implem.bugfinder]
-p:28 [in WiSE.implem.bugfinder]
-p:30 [in WiSE.implem.bugfinder]
-p:48 [in WiSE.implem.bugfinder_proof]
-p:5 [in WiSE.implem.bugfinder]
-p:67 [in WiSE.implem.bugfinder_proof]
-P:68 [in WiSE.streams]
-p:68 [in WiSE.implem.bugfinder_proof]
-p:70 [in WiSE.implem.bugfinder_proof]
-P:71 [in WiSE.streams]
-p:73 [in WiSE.implem.bugfinder_proof]
-P:75 [in WiSE.streams]
-P:79 [in WiSE.streams]
-p:79 [in WiSE.implem.bugfinder_proof]
-p:81 [in WiSE.implem.bugfinder_proof]
-p:82 [in WiSE.implem.bugfinder_proof]
-P:83 [in WiSE.streams]
-P:87 [in WiSE.streams]
-P:91 [in WiSE.streams]
-P:94 [in WiSE.streams]
-

Q

-Q:120 [in WiSE.streams]
-q:4 [in WiSE.implem.bugfinder]
-Q:80 [in WiSE.streams]
-Q:84 [in WiSE.streams]
-Q:88 [in WiSE.streams]
-

R

-RA:21 [in WiSE.relations]
-RA:30 [in WiSE.relations]
-RB:22 [in WiSE.relations]
-RB:31 [in WiSE.relations]
-

S

-senv1:63 [in WiSE.symbolic.symex]
-senv1:71 [in WiSE.symbolic.symex]
-senv1:80 [in WiSE.symbolic.symex]
-senv1:88 [in WiSE.symbolic.symex]
-senv1:95 [in WiSE.symbolic.symex]
-senv2:64 [in WiSE.symbolic.symex]
-senv2:74 [in WiSE.symbolic.symex]
-senv2:83 [in WiSE.symbolic.symex]
-senv2:89 [in WiSE.symbolic.symex]
-senv2:96 [in WiSE.symbolic.symex]
-senv:103 [in WiSE.symbolic.symex]
-senv:111 [in WiSE.symbolic.symex]
-senv:127 [in WiSE.symbolic.symex]
-senv:135 [in WiSE.symbolic.symex]
-senv:19 [in WiSE.symbolic.symex]
-senv:22 [in WiSE.symbolic.symex]
-senv:25 [in WiSE.symbolic.symex]
-sim:23 [in WiSE.relations]
-sim:32 [in WiSE.relations]
-str:101 [in WiSE.streams]
-str:65 [in WiSE.streams]
-st:150 [in WiSE.lang.imp]
-st:24 [in WiSE.implem.bugfinder]
-st:43 [in WiSE.implem.bugfinder_proof]
-st:46 [in WiSE.implem.bugfinder_proof]
-st:49 [in WiSE.implem.bugfinder_proof]
-st:51 [in WiSE.implem.bugfinder_proof]
-st:53 [in WiSE.implem.bugfinder_proof]
-st:74 [in WiSE.implem.bugfinder_proof]
-st:77 [in WiSE.implem.bugfinder_proof]
-s'':77 [in WiSE.lang.imp]
-s'':92 [in WiSE.lang.imp]
-s':121 [in WiSE.symbolic.symex]
-s':123 [in WiSE.symbolic.symex]
-s':136 [in WiSE.lang.imp]
-s':144 [in WiSE.lang.imp]
-s':148 [in WiSE.lang.imp]
-s':181 [in WiSE.lang.imp]
-s':58 [in WiSE.implem.bugfinder_proof]
-s':61 [in WiSE.implem.bugfinder_proof]
-s':64 [in WiSE.implem.bugfinder_proof]
-s':69 [in WiSE.implem.bugfinder_proof]
-s':76 [in WiSE.lang.imp]
-s':81 [in WiSE.lang.imp]
-s':86 [in WiSE.lang.imp]
-s':91 [in WiSE.lang.imp]
-s0:41 [in WiSE.implem.bugfinder_proof]
-s1:104 [in WiSE.lang.imp]
-s1:125 [in WiSE.streams]
-s1:129 [in WiSE.lang.imp]
-s1:139 [in WiSE.lang.imp]
-s1:19 [in WiSE.implem.bugfinder_proof]
-s1:37 [in WiSE.symbolic.symex]
-s2:105 [in WiSE.lang.imp]
-s2:126 [in WiSE.streams]
-s2:130 [in WiSE.lang.imp]
-s2:140 [in WiSE.lang.imp]
-s2:20 [in WiSE.implem.bugfinder_proof]
-s2:38 [in WiSE.symbolic.symex]
-s3:141 [in WiSE.lang.imp]
-s:10 [in WiSE.symbolic.symex]
-s:10 [in WiSE.streams]
-s:100 [in WiSE.lang.imp]
-s:104 [in WiSE.streams]
-s:107 [in WiSE.streams]
-s:109 [in WiSE.lang.imp]
-s:110 [in WiSE.streams]
-s:111 [in WiSE.lang.imp]
-s:114 [in WiSE.streams]
-s:115 [in WiSE.lang.imp]
-s:118 [in WiSE.streams]
-s:119 [in WiSE.lang.imp]
-s:120 [in WiSE.symbolic.symex]
-s:122 [in WiSE.symbolic.symex]
-s:122 [in WiSE.lang.imp]
-s:13 [in WiSE.streams]
-s:135 [in WiSE.lang.imp]
-s:14 [in WiSE.symbolic.symex]
-s:143 [in WiSE.lang.imp]
-s:146 [in WiSE.lang.imp]
-s:165 [in WiSE.lang.imp]
-s:172 [in WiSE.lang.imp]
-s:18 [in WiSE.implem.bugfinder_proof]
-s:180 [in WiSE.lang.imp]
-s:19 [in WiSE.streams]
-s:2 [in WiSE.symbolic.symex]
-s:22 [in WiSE.lang.imprec]
-s:24 [in WiSE.streams]
-s:24 [in WiSE.lang.imp]
-s:3 [in WiSE.implem.bugfinder]
-s:30 [in WiSE.symbolic.symex]
-s:33 [in WiSE.streams]
-s:36 [in WiSE.implem.bugfinder]
-s:36 [in WiSE.lang.imp]
-s:39 [in WiSE.implem.bugfinder_proof]
-s:40 [in WiSE.streams]
-s:42 [in WiSE.symbolic.symex]
-s:42 [in WiSE.implem.bugfinder_proof]
-s:45 [in WiSE.symbolic.symex]
-s:45 [in WiSE.implem.bugfinder_proof]
-s:48 [in WiSE.lang.imp]
-s:50 [in WiSE.symbolic.symex]
-s:50 [in WiSE.streams]
-s:52 [in WiSE.lang.imp]
-s:55 [in WiSE.symbolic.symex]
-s:55 [in WiSE.streams]
-s:56 [in WiSE.lang.imp]
-s:57 [in WiSE.implem.bugfinder_proof]
-s:59 [in WiSE.symbolic.symex]
-s:59 [in WiSE.implem.bugfinder_proof]
-s:60 [in WiSE.implem.bugfinder_proof]
-s:60 [in WiSE.lang.imp]
-s:61 [in WiSE.streams]
-s:63 [in WiSE.implem.bugfinder_proof]
-s:64 [in WiSE.lang.imp]
-s:69 [in WiSE.streams]
-s:7 [in WiSE.symbolic.symex]
-s:7 [in WiSE.streams]
-s:70 [in WiSE.lang.imp]
-s:71 [in WiSE.lang.imp]
-s:72 [in WiSE.streams]
-s:75 [in WiSE.lang.imp]
-s:76 [in WiSE.streams]
-s:80 [in WiSE.lang.imp]
-s:81 [in WiSE.streams]
-s:85 [in WiSE.streams]
-s:85 [in WiSE.lang.imp]
-s:89 [in WiSE.streams]
-s:90 [in WiSE.lang.imp]
-s:92 [in WiSE.streams]
-s:95 [in WiSE.streams]
-s:95 [in WiSE.lang.imp]
-

T

-tasks:19 [in WiSE.implem.bugfinder]
-tasks:38 [in WiSE.implem.bugfinder_proof]
-t:10 [in WiSE.implem.bugfinder_proof]
-t:14 [in WiSE.implem.bugfinder_proof]
-

V

-ve:103 [in WiSE.lang.imp]
-ve:34 [in WiSE.symbolic.symex]
-ve:74 [in WiSE.lang.imp]
-vx:35 [in WiSE.lang.imp]
-vx:47 [in WiSE.lang.imp]
-vx:63 [in WiSE.lang.imp]
-vx:67 [in WiSE.lang.imp]
-V0:141 [in WiSE.symbolic.symex]
-V0:148 [in WiSE.symbolic.symex]
-V0:159 [in WiSE.symbolic.symex]
-V0:163 [in WiSE.symbolic.symex]
-V0:188 [in WiSE.lang.imp]
-V0:194 [in WiSE.lang.imp]
-V:196 [in WiSE.lang.imp]
-v:50 [in WiSE.lang.imp]
-

X

-xs:13 [in WiSE.utils]
-xs:18 [in WiSE.utils]
-xs:30 [in WiSE.streams]
-xs:47 [in WiSE.streams]
-xs:5 [in WiSE.streams]
-x:1 [in WiSE.symbolic.symex]
-x:101 [in WiSE.lang.imp]
-x:102 [in WiSE.streams]
-x:128 [in WiSE.lang.imp]
-x:13 [in WiSE.relations]
-x:14 [in WiSE.relations]
-x:143 [in WiSE.streams]
-x:145 [in WiSE.streams]
-x:15 [in WiSE.lang.imprec]
-x:157 [in WiSE.lang.imp]
-x:17 [in WiSE.relations]
-x:19 [in WiSE.lang.imprec]
-x:23 [in WiSE.lang.imprec]
-x:27 [in WiSE.symbolic.symex]
-x:29 [in WiSE.lang.imprec]
-x:29 [in WiSE.streams]
-x:29 [in WiSE.lang.imp]
-x:3 [in WiSE.lang.imprec]
-x:3 [in WiSE.symbolic.symex]
-x:32 [in WiSE.symbolic.symex]
-x:32 [in WiSE.implem.bugfinder]
-x:34 [in WiSE.implem.bugfinder]
-x:34 [in WiSE.lang.imp]
-x:4 [in WiSE.lang.imprec]
-x:4 [in WiSE.streams]
-x:41 [in WiSE.lang.imp]
-x:46 [in WiSE.streams]
-x:46 [in WiSE.lang.imp]
-x:49 [in WiSE.lang.imp]
-x:5 [in WiSE.relations]
-x:54 [in WiSE.lang.imp]
-x:58 [in WiSE.lang.imp]
-x:6 [in WiSE.relations]
-x:62 [in WiSE.lang.imp]
-x:66 [in WiSE.lang.imp]
-x:72 [in WiSE.lang.imp]
-X:77 [in WiSE.symbolic.symex]
-x:8 [in WiSE.symbolic.symex]
-X:86 [in WiSE.symbolic.symex]
-x:9 [in WiSE.relations]
-x:96 [in WiSE.streams]
-

Y

-y:10 [in WiSE.relations]
-y:15 [in WiSE.relations]
-y:18 [in WiSE.relations]
-y:5 [in WiSE.symbolic.symex]
-y:51 [in WiSE.lang.imp]
-y:6 [in WiSE.utils]
-y:7 [in WiSE.relations]
-Y:78 [in WiSE.symbolic.symex]
-Y:87 [in WiSE.symbolic.symex]
-

Z

-z:16 [in WiSE.relations]
-z:8 [in WiSE.relations]
-

other

-π1:35 [in WiSE.symbolic.symex]
-π1:65 [in WiSE.symbolic.symex]
-π1:70 [in WiSE.symbolic.symex]
-π1:79 [in WiSE.symbolic.symex]
-π1:90 [in WiSE.symbolic.symex]
-π1:97 [in WiSE.symbolic.symex]
-π2:36 [in WiSE.symbolic.symex]
-π2:66 [in WiSE.symbolic.symex]
-π2:73 [in WiSE.symbolic.symex]
-π2:82 [in WiSE.symbolic.symex]
-π2:91 [in WiSE.symbolic.symex]
-π2:98 [in WiSE.symbolic.symex]
-π:101 [in WiSE.symbolic.symex]
-π:112 [in WiSE.symbolic.symex]
-π:134 [in WiSE.symbolic.symex]
-π:31 [in WiSE.symbolic.symex]
-π:44 [in WiSE.symbolic.symex]
-π:49 [in WiSE.symbolic.symex]
-π:54 [in WiSE.symbolic.symex]
-π:58 [in WiSE.symbolic.symex]
-σ':142 [in WiSE.symbolic.symex]
-σ':150 [in WiSE.symbolic.symex]
-σ':162 [in WiSE.symbolic.symex]
-σ':71 [in WiSE.implem.bugfinder_proof]
-σ:139 [in WiSE.symbolic.symex]
-σ:140 [in WiSE.symbolic.symex]
-σ:144 [in WiSE.symbolic.symex]
-σ:146 [in WiSE.symbolic.symex]
-σ:149 [in WiSE.symbolic.symex]
-σ:152 [in WiSE.symbolic.symex]
-σ:154 [in WiSE.symbolic.symex]
-σ:157 [in WiSE.symbolic.symex]
-σ:160 [in WiSE.symbolic.symex]
-σ:161 [in WiSE.symbolic.symex]
-σ:183 [in WiSE.lang.imp]
-σ:186 [in WiSE.lang.imp]
-σ:187 [in WiSE.lang.imp]
-σ:190 [in WiSE.lang.imp]
-σ:192 [in WiSE.lang.imp]
-σ:195 [in WiSE.lang.imp]
-σ:72 [in WiSE.implem.bugfinder_proof]
-σ:76 [in WiSE.implem.bugfinder_proof]
-σ:80 [in WiSE.implem.bugfinder_proof]
-

-

Module Index

-

L

-LTL [in WiSE.streams]
-

-

Variable Index

-

S

-Sequences.A [in WiSE.relations]
-Sequences.R [in WiSE.relations]
-

-

Library Index

-

B

-bugfinder
-bugfinder_proof
-

E

-equalities
-extract
-

I

-imp
-imprec
-

R

-relations
-

S

-solver
-streams
-symex
-

U

-utils
-

-

Constructor Index

-

A

-Add [in WiSE.lang.imprec]
-Add [in WiSE.lang.imp]
-Aff [in WiSE.lang.imprec]
-Aff [in WiSE.lang.imp]
-

B

-Band [in WiSE.lang.imprec]
-Band [in WiSE.lang.imp]
-Bcst [in WiSE.lang.imprec]
-Bcst [in WiSE.lang.imp]
-Beq [in WiSE.lang.imprec]
-Beq [in WiSE.lang.imp]
-Ble [in WiSE.lang.imprec]
-Ble [in WiSE.lang.imp]
-Bnot [in WiSE.lang.imprec]
-Bnot [in WiSE.lang.imp]
-BugFound [in WiSE.implem.bugfinder]
-

C

-Cst [in WiSE.lang.imprec]
-Cst [in WiSE.lang.imp]
-

E

-EQ [in WiSE.equalities]
-Err [in WiSE.lang.imprec]
-Err [in WiSE.lang.imp]
-error_Seq [in WiSE.lang.imp]
-error_Err [in WiSE.lang.imp]
-exec_loop_false [in WiSE.lang.imp]
-exec_loop_true [in WiSE.lang.imp]
-exec_Ite_false [in WiSE.lang.imp]
-exec_Ite_true [in WiSE.lang.imp]
-exec_Seq [in WiSE.lang.imp]
-exec_Aff [in WiSE.lang.imp]
-exec_Skip [in WiSE.lang.imp]
-

F

-Finished [in WiSE.implem.bugfinder]
-

G

-Global [in WiSE.lang.imprec]
-

I

-Ite [in WiSE.lang.imprec]
-Ite [in WiSE.lang.imp]
-

L

-Local [in WiSE.lang.imprec]
-Loop [in WiSE.lang.imprec]
-Loop [in WiSE.lang.imp]
-

M

-MAYBE [in WiSE.symbolic.solver]
-

P

-Pending [in WiSE.implem.bugfinder]
-

S

-SAT [in WiSE.symbolic.solver]
-scons [in WiSE.streams]
-Seq [in WiSE.lang.imprec]
-Seq [in WiSE.lang.imp]
-Skip [in WiSE.lang.imprec]
-Skip [in WiSE.lang.imp]
-starr_step [in WiSE.relations]
-starr_refl [in WiSE.relations]
-star_step [in WiSE.relations]
-star_refl [in WiSE.relations]
-step_Loop_false [in WiSE.lang.imp]
-step_Loop_true [in WiSE.lang.imp]
-step_Ite_false [in WiSE.lang.imp]
-step_Ite_true [in WiSE.lang.imp]
-step_Seq_Skip [in WiSE.lang.imp]
-step_Seq [in WiSE.lang.imp]
-step_Aff [in WiSE.lang.imp]
-Sub [in WiSE.lang.imprec]
-Sub [in WiSE.lang.imp]
-sym_step_Loop_false [in WiSE.symbolic.symex]
-sym_step_Loop_true [in WiSE.symbolic.symex]
-sym_step_Ite_false [in WiSE.symbolic.symex]
-sym_step_Ite_true [in WiSE.symbolic.symex]
-sym_step_Seq_Skip [in WiSE.symbolic.symex]
-sym_step_Seq [in WiSE.symbolic.symex]
-sym_step_Aff [in WiSE.symbolic.symex]
-

U

-UNSAT [in WiSE.symbolic.solver]
-

V

-Var [in WiSE.lang.imprec]
-Var [in WiSE.lang.imp]
-

-

Lemma Index

-

A

-aeq_spec [in WiSE.lang.imp]
-aeval_comp [in WiSE.symbolic.symex]
-aeval_stable [in WiSE.lang.imp]
-aeval_inst [in WiSE.lang.imp]
-aeval_asubst [in WiSE.lang.imp]
-asimp_correct [in WiSE.symbolic.solver]
-

B

-BadInput_correct [in WiSE.symbolic.symex]
-beq_spec [in WiSE.lang.imp]
-beval_comp [in WiSE.symbolic.symex]
-beval_inst [in WiSE.lang.imp]
-beval_bsubst [in WiSE.lang.imp]
-bsimp_correct [in WiSE.symbolic.solver]
-

C

-comp_update [in WiSE.symbolic.symex]
-comp_id [in WiSE.symbolic.symex]
-

E

-error_state_error [in WiSE.lang.imp]
-error_state_seq [in WiSE.lang.imp]
-exec_steps [in WiSE.lang.imp]
-expand_inv [in WiSE.implem.bugfinder_proof]
-expand_complete [in WiSE.implem.bugfinder_proof]
-expand_sound [in WiSE.implem.bugfinder_proof]
-

F

-find_bugs_complete [in WiSE.implem.bugfinder_proof]
-find_bugs_sound [in WiSE.implem.bugfinder_proof]
-force_id [in WiSE.streams]
-func_to_stream_correct [in WiSE.streams]
-

G

-get_map [in WiSE.streams]
-get_filter [in WiSE.streams]
-get_shift [in WiSE.streams]
-

H

-HasBug_correct [in WiSE.symbolic.symex]
-

I

-IsBug_correct [in WiSE.symbolic.symex]
-is_error_Stuck [in WiSE.lang.imp]
-is_error_correct [in WiSE.lang.imp]
-

L

-LTL.globally_map [in WiSE.streams]
-LTL.shift_shift [in WiSE.streams]
-

M

-map_eq [in WiSE.streams]
-map_in [in WiSE.implem.bugfinder_proof]
-mk_not_correct [in WiSE.symbolic.solver]
-mk_and_correct [in WiSE.symbolic.solver]
-mk_sub_correct [in WiSE.symbolic.solver]
-mk_add_correct [in WiSE.symbolic.solver]
-

P

-progress_Loop [in WiSE.lang.imp]
-progress_Seq [in WiSE.lang.imp]
-progress_Aff [in WiSE.lang.imp]
-progress_Ite [in WiSE.lang.imp]
-progress_Skip [in WiSE.lang.imp]
-

R

-Reach_complete [in WiSE.symbolic.symex]
-Reach_sound [in WiSE.symbolic.symex]
-relative_soundness [in WiSE.implem.bugfinder_proof]
-relative_completeness [in WiSE.implem.bugfinder_proof]
-run_finished [in WiSE.implem.bugfinder_proof]
-run_finished_nil [in WiSE.implem.bugfinder_proof]
-run_complete [in WiSE.implem.bugfinder_proof]
-run_steps_complete [in WiSE.implem.bugfinder_proof]
-run_here [in WiSE.implem.bugfinder_proof]
-run_step_complete [in WiSE.implem.bugfinder_proof]
-run_sound [in WiSE.implem.bugfinder_proof]
-run_n_S_length [in WiSE.implem.bugfinder_proof]
-run_n_length [in WiSE.implem.bugfinder_proof]
-run_n_nil [in WiSE.implem.bugfinder_proof]
-run_run_n [in WiSE.implem.bugfinder_proof]
-run_nil [in WiSE.implem.bugfinder_proof]
-run_eq [in WiSE.implem.bugfinder_proof]
-

S

-shift_eq [in WiSE.streams]
-sim_init [in WiSE.symbolic.symex]
-solver_correct [in WiSE.symbolic.solver]
-sound_termination [in WiSE.implem.bugfinder_proof]
-starr_star [in WiSE.relations]
-star_simulation [in WiSE.relations]
-star_one [in WiSE.relations]
-steps_simulation_diagram [in WiSE.symbolic.symex]
-steps_exec [in WiSE.lang.imp]
-steps_seq [in WiSE.lang.imp]
-step_simulation_diagram [in WiSE.symbolic.symex]
-step_exec_exec [in WiSE.lang.imp]
-stream_func_iso [in WiSE.streams]
-symex_complete [in WiSE.symbolic.symex]
-symex_sound [in WiSE.symbolic.symex]
-sym_steps_steps [in WiSE.symbolic.symex]
-sym_steps_steps_aux [in WiSE.symbolic.symex]
-sym_steps_path [in WiSE.symbolic.symex]
-sym_step_path [in WiSE.symbolic.symex]
-sym_step_step [in WiSE.symbolic.symex]
-

-

Projection Index

-

B

-body [in WiSE.lang.imprec]
-

D

-decls [in WiSE.lang.imprec]
-

E

-eq_op [in WiSE.equalities]
-

H

-Hlocals [in WiSE.lang.imprec]
-

M

-main [in WiSE.lang.imprec]
-

P

-params [in WiSE.lang.imprec]
-

-

Inductive Index

-

A

-aexpr [in WiSE.lang.imprec]
-aexpr [in WiSE.lang.imp]
-

B

-bexpr [in WiSE.lang.imprec]
-bexpr [in WiSE.lang.imp]
-

E

-error [in WiSE.lang.imp]
-exec [in WiSE.lang.imp]
-

I

-IMP [in WiSE.lang.imp]
-

S

-sat [in WiSE.symbolic.solver]
-star [in WiSE.relations]
-starr [in WiSE.relations]
-status [in WiSE.implem.bugfinder]
-step [in WiSE.lang.imp]
-stmt [in WiSE.lang.imprec]
-stream [in WiSE.streams]
-sym_step [in WiSE.symbolic.symex]
-

V

-variable [in WiSE.lang.imprec]
-

-

Instance Index

-

F

-fun_Eq [in WiSE.streams]
-

S

-starr_reflexive [in WiSE.relations]
-starr_trans [in WiSE.relations]
-star_trans [in WiSE.relations]
-star_reflexive [in WiSE.relations]
-stream_Eq [in WiSE.streams]
-

-

Section Index

-

E

-Examples [in WiSE.implem.bugfinder]
-Examples.Gcd [in WiSE.implem.bugfinder]
-Examples.Simple [in WiSE.implem.bugfinder]
-

S

-Sequences [in WiSE.relations]
-Simulation [in WiSE.relations]
-

-

Definition Index

-

A

-a [in WiSE.implem.bugfinder]
-aeq [in WiSE.lang.imp]
-aeval [in WiSE.lang.imprec]
-aeval [in WiSE.lang.imp]
-ainst [in WiSE.lang.imp]
-all_some [in WiSE.utils]
-alocals [in WiSE.lang.imprec]
-asimp [in WiSE.symbolic.solver]
-Assert [in WiSE.lang.imprec]
-Assert [in WiSE.lang.imp]
-asubst [in WiSE.lang.imp]
-a0 [in WiSE.implem.bugfinder]
-

B

-b [in WiSE.implem.bugfinder]
-BadInput [in WiSE.symbolic.symex]
-BadInput [in WiSE.lang.imp]
-beq [in WiSE.lang.imp]
-beval [in WiSE.lang.imp]
-bijection [in WiSE.equalities]
-binst [in WiSE.lang.imp]
-blocals [in WiSE.lang.imprec]
-Bor [in WiSE.lang.imprec]
-Bor [in WiSE.lang.imp]
-bsimp [in WiSE.symbolic.solver]
-bsubst [in WiSE.lang.imp]
-bug [in WiSE.lang.imp]
-bug_found [in WiSE.implem.bugfinder_proof]
-b0 [in WiSE.implem.bugfinder]
-

C

-comp [in WiSE.symbolic.symex]
-complete_bug_finding [in WiSE.symbolic.symex]
-Concrete [in WiSE.symbolic.symex]
-

D

-display [in WiSE.implem.bugfinder]
-done [in WiSE.implem.bugfinder_proof]
-

E

-enum [in WiSE.streams]
-enum_equ [in WiSE.streams]
-error_state [in WiSE.lang.imp]
-eventually [in WiSE.streams]
-execute_gcd_err [in WiSE.implem.bugfinder]
-execute_gcd_noerr [in WiSE.implem.bugfinder]
-execute_gcd [in WiSE.implem.bugfinder]
-expand [in WiSE.implem.bugfinder]
-

F

-filter [in WiSE.streams]
-find_bugs_assuming [in WiSE.implem.bugfinder]
-find_bugs [in WiSE.implem.bugfinder]
-first [in WiSE.utils]
-force [in WiSE.streams]
-func_to_stream [in WiSE.streams]
-

G

-gcd [in WiSE.implem.bugfinder]
-gcd_buggy [in WiSE.implem.bugfinder]
-gcd_assertions [in WiSE.implem.bugfinder]
-get [in WiSE.streams]
-globally [in WiSE.streams]
-global_store [in WiSE.lang.imprec]
-

H

-HasBug [in WiSE.symbolic.symex]
-HasBug [in WiSE.lang.imp]
-here [in WiSE.implem.bugfinder_proof]
-

I

-id [in WiSE.symbolic.symex]
-ident [in WiSE.lang.imprec]
-ident [in WiSE.lang.imp]
-init [in WiSE.implem.bugfinder]
-init_store' [in WiSE.implem.bugfinder]
-init_store [in WiSE.implem.bugfinder]
-init_assuming [in WiSE.implem.bugfinder]
-IsBug [in WiSE.symbolic.symex]
-IsBug [in WiSE.lang.imp]
-isomorph [in WiSE.equalities]
-is_sat [in WiSE.symbolic.solver]
-is_skip [in WiSE.lang.imp]
-is_error [in WiSE.lang.imp]
-

L

-locals [in WiSE.lang.imprec]
-local_store [in WiSE.lang.imprec]
-LTL.and [in WiSE.streams]
-LTL.eventually [in WiSE.streams]
-LTL.globally [in WiSE.streams]
-LTL.imp [in WiSE.streams]
-LTL.model [in WiSE.streams]
-LTL.next [in WiSE.streams]
-LTL.not [in WiSE.streams]
-LTL.now [in WiSE.streams]
-LTL.or [in WiSE.streams]
-LTL.t [in WiSE.streams]
-

M

-map [in WiSE.streams]
-map_opt [in WiSE.utils]
-mk_not [in WiSE.symbolic.solver]
-mk_and [in WiSE.symbolic.solver]
-mk_sub [in WiSE.symbolic.solver]
-mk_add [in WiSE.symbolic.solver]
-my_prog [in WiSE.implem.bugfinder]
-

N

-none [in WiSE.implem.bugfinder_proof]
-now [in WiSE.streams]
-

P

-peek [in WiSE.streams]
-potential_bug [in WiSE.symbolic.symex]
-potential_bug [in WiSE.implem.bugfinder_proof]
-progress [in WiSE.lang.imp]
-

R

-Reach [in WiSE.symbolic.symex]
-Reach [in WiSE.lang.imp]
-reachable_from [in WiSE.implem.bugfinder_proof]
-reduce [in WiSE.utils]
-relatively_sound_bug_finding [in WiSE.symbolic.symex]
-run [in WiSE.implem.bugfinder]
-run_n [in WiSE.implem.bugfinder]
-

S

-shift [in WiSE.streams]
-sim [in WiSE.symbolic.symex]
-simulation [in WiSE.relations]
-solver [in WiSE.symbolic.solver]
-steps [in WiSE.lang.imp]
-store [in WiSE.lang.imp]
-stream_equ [in WiSE.streams]
-Stuck [in WiSE.lang.imp]
-Symbolic [in WiSE.implem.bugfinder_proof]
-sym_steps [in WiSE.symbolic.symex]
-sym_state [in WiSE.symbolic.symex]
-sym_beval [in WiSE.symbolic.symex]
-sym_aeval [in WiSE.symbolic.symex]
-sym_update [in WiSE.symbolic.symex]
-sym_store [in WiSE.symbolic.symex]
-

T

-tasks [in WiSE.implem.bugfinder]
-then_do [in WiSE.implem.bugfinder]
-trivial_assertion [in WiSE.implem.bugfinder]
-

U

-untill [in WiSE.streams]
-update [in WiSE.lang.imp]
-

V

-ValidBug [in WiSE.implem.bugfinder_proof]
-ValidStatus [in WiSE.implem.bugfinder_proof]
-

-

Record Index

-

D

-declaration [in WiSE.lang.imprec]
-

E

-Eq [in WiSE.equalities]
-

I

-IMPREC [in WiSE.lang.imprec]
-

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Global IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(986 entries)
Notation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(17 entries)
Binder IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(649 entries)
Module IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1 entry)
Variable IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(2 entries)
Library IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(11 entries)
Constructor IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(67 entries)
Lemma IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(81 entries)
Projection IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(6 entries)
Inductive IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(16 entries)
Instance IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(6 entries)
Section IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(5 entries)
Definition IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(122 entries)
Record IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(3 entries)
-
- -
- - - diff --git a/html/toc.html b/html/toc.html deleted file mode 100644 index d17451b..0000000 --- a/html/toc.html +++ /dev/null @@ -1,143 +0,0 @@ - - - - - - - - - - - - - -
- - -
- - - diff --git a/src/implem/bugfinder_proof.v b/src/implem/bugfinder_proof.v index f1858f8..05edfe5 100644 --- a/src/implem/bugfinder_proof.v +++ b/src/implem/bugfinder_proof.v @@ -330,7 +330,7 @@ Qed. Theorem run_finished_nil: forall l, - none (run l) -> l = []. + run l ⊨ none -> l = []. Proof. now intros [|[[path env] prog]]. Qed. @@ -438,43 +438,20 @@ Theorem relative_soundness: forall p, find_bugs p ⊨ □ ValidStatus p. Proof. - intros. - (* cleary a reformulation of find_bugs_sound *) -Admitted. - -(** ** Main Correctness Theorem !!!! *) - -(** THE MAIN RESULT: - [find_bugs p] is correct ! - This statement means 2 things: - (1) For any bug in the program [p], the bug is eventually going - to be discovered - (2) If a 'bugy path' is discovered, then any concrete - instance of this path is a bug -*) -(* Theorem find_bugs_correct: - forall env0 prog0 env1 prog1, - imp.bug (env0, prog0) (env1, prog1) <-> - exists path2 env2 prog2, - simpath (env0, prog0) (env1, prog1) (path2, env2, prog2) /\ - (◊ (bug_found (path2, env2, prog2))) (find_bugs prog0). -Proof. - intros. split. - + intros (path2 & env2 & prog2 & [Hbug Hpath])%bug_bug. - do 3 eexists. split; eauto. - now apply find_bugs_sym_complete. - + intros (path2 & env2 & prog2 & [Hpath [n Hbug]]). - pose proof (H1 := find_bugs_sym_sound prog0 n). - pose proof (H2 := bug_found_bug_here _ _ Hbug). - specialize (H1 H2). - unfold bug_from, bug_found, now, here in *. - rewrite get_shift in *. - destruct get eqn:Heq; subst; try easy. - destruct Hpath as [H [-> ->]]. - apply bug_bug. - do 3 eexists. split; eauto. - now repeat econstructor. -Qed. *) + intros p n. + pose proof (find_bugs_sound p n). + unfold ValidStatus, potential_bug, now, get in *. + destruct (shift) eqn:Heq. + destruct x as [ [[φ senv] p'] | | ]; auto. + intros [V p''] (V0 & HV0). + destruct H as [H2 H3]. + split. + - apply symex.Reach_sound. + now exists V0, (φ, senv, p'). + - destruct HV0 as [_ [_ <-]]. + now apply is_error_Stuck, is_error_correct. +Qed. + (** "termination" of the bugfinding loop: If at any point in time [find_bugs p] emits