mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 09:40:21 +00:00
4f1e5c34b1
BSD-2-Clause: https://github.com/jscert/jscert * JSCorrectness.v * JSInterpreterExtraction.v * JSNumber.v * JSPrettyInterm.v MIT/Expat: https://github.com/clarus/coq-atm * Computation.v * Main.v * Spec.v
63 lines
1.9 KiB
Coq
63 lines
1.9 KiB
Coq
(** Specifications. *)
|
|
Require Import Coq.Lists.List.
|
|
Require Import Coq.Strings.Ascii.
|
|
Require Import FunctionNinjas.All.
|
|
Require Import ListString.All.
|
|
Require Import Computation.
|
|
|
|
Import ListNotations.
|
|
Local Open Scope char.
|
|
|
|
(** A run is an execution of the program with explicit answers for the
|
|
system calls. *)
|
|
Module Run.
|
|
(** We define a run by induction on the structure of a computation. *)
|
|
Inductive t : C.t -> Type :=
|
|
| Ret : t C.Ret
|
|
| Call : forall (command : Command.t) (answer : Command.answer command)
|
|
{handler : Command.answer command -> C.t}, t (handler answer) ->
|
|
t (C.Call command handler).
|
|
|
|
(** The trace of a run. *)
|
|
Fixpoint trace {x : C.t} (run : t x)
|
|
: list {command : Command.t & Command.answer command} :=
|
|
match run with
|
|
| Ret => []
|
|
| Call command answer _ run => existT _ command answer :: trace run
|
|
end.
|
|
End Run.
|
|
|
|
Module Temporal.
|
|
Module All.
|
|
Inductive t (P : Command.t -> Prop) : C.t -> Prop :=
|
|
| Ret : t P C.Ret
|
|
| Call : forall (c : Command.t) (h : Command.answer c -> C.t),
|
|
P c -> (forall a, t P (h a)) ->
|
|
t P (C.Call c h).
|
|
End All.
|
|
|
|
Module One.
|
|
Inductive t (P : Command.t -> Prop) : C.t -> Prop :=
|
|
| CallThis : forall (c : Command.t) (h : Command.answer c -> C.t),
|
|
P c ->
|
|
t P (C.Call c h)
|
|
| CallOther : forall (c : Command.t) (h : Command.answer c -> C.t),
|
|
(forall a, t P (h a)) ->
|
|
t P (C.Call c h).
|
|
End One.
|
|
|
|
Module Then.
|
|
Inductive t (P1 P2 : Command.t -> Prop) : C.t -> Prop :=
|
|
| Ret : t P1 P2 C.Ret
|
|
| Call : forall (c : Command.t) (h : Command.answer c -> C.t),
|
|
(forall a, t P1 P2 (h a)) ->
|
|
t P1 P2 (C.Call c h)
|
|
| CallThen : forall (c : Command.t) (h : Command.answer c -> C.t),
|
|
P1 c -> (forall a, One.t P2 (h a)) ->
|
|
t P1 P2 (C.Call c h).
|
|
End Then.
|
|
End Temporal.
|
|
|
|
Module CardBeforeMoney.
|
|
End CardBeforeMoney.
|