inductive
Imperative.EvalNondetStmt
(P : PureExpr)
(Cmd : Type)
(EvalCmd : EvalCmdParam P Cmd)
[HasVarsImp P (List (Stmt P Cmd))]
[HasVarsImp P Cmd]
[HasFvar P]
[HasBool P]
[HasNot P]
:
SemanticEval P → SemanticStore P → NondetStmt P Cmd → SemanticStore P → Prop
An inductively-defined operational semantics for non-deterministic statements that depends on environment lookup and evaluation functions for expressions. NOTE: This will probably be replaced with a small-step semantics. Note: Nondeterministic statements don't track evaluator changes since commands preserve the evaluator (only funcDecl statements modify it).
- cmd_sem {P : PureExpr} {Cmd : Type} {EvalCmd : EvalCmdParam P Cmd} [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasBool P] [HasNot P] {δ : SemanticEval P} {σ : SemanticStore P} {c : Cmd} {σ' : SemanticStore P} : EvalCmd δ σ c σ' → isDefinedOver HasVarsImp.modifiedVars σ c → EvalNondetStmt P Cmd EvalCmd δ σ (NondetStmt.cmd c) σ'
- seq_sem {P : PureExpr} {Cmd : Type} {EvalCmd : EvalCmdParam P Cmd} [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasBool P] [HasNot P] {δ : SemanticEval P} {σ : SemanticStore P} {s1 : NondetStmt P Cmd} {σ' : SemanticStore P} {s2 : NondetStmt P Cmd} {σ'' : SemanticStore P} : EvalNondetStmt P Cmd EvalCmd δ σ s1 σ' → EvalNondetStmt P Cmd EvalCmd δ σ' s2 σ'' → EvalNondetStmt P Cmd EvalCmd δ σ (s1.seq s2) σ''
- choice_left_sem {P : PureExpr} {Cmd : Type} {EvalCmd : EvalCmdParam P Cmd} [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasBool P] [HasNot P] {δ : SemanticEval P} {σ : SemanticStore P} {s1 : NondetStmt P Cmd} {σ' : SemanticStore P} {s2 : NondetStmt P Cmd} : WellFormedSemanticEvalBool δ → EvalNondetStmt P Cmd EvalCmd δ σ s1 σ' → EvalNondetStmt P Cmd EvalCmd δ σ (s1.choice s2) σ'
- choice_right_sem {P : PureExpr} {Cmd : Type} {EvalCmd : EvalCmdParam P Cmd} [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasBool P] [HasNot P] {δ : SemanticEval P} {σ : SemanticStore P} {s2 : NondetStmt P Cmd} {σ' : SemanticStore P} {s1 : NondetStmt P Cmd} : WellFormedSemanticEvalBool δ → EvalNondetStmt P Cmd EvalCmd δ σ s2 σ' → EvalNondetStmt P Cmd EvalCmd δ σ (s1.choice s2) σ'