weblib/While/semantics.ma

   1 (* new script *)
   2
   3 include "While/syntax.ma".
   4 include "arithmetics/div_and_mod.ma.
   5
   6
   7 (* state *)
   8
   9 definition state ≝ \ 5a href="cic:/matita/While/syntax/Var.ind(1,0,0)"\ 6Var\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
  10
  11 (* Semantics of Arithmetic expressions *)
  12
  13 \ 5pre class="smallmargin" style="display: inline;"\ 6let rec eval_Aexp a s ≝
  14   match a with
  15   | Const n => n
  16   | Aid v => s v
  17   | Add a b => a+b
  18   | Sub a b => a-b
  19   | Mul a b => a*b
  20   | Div a b => div a b
  21   | Mod a b => mod a b
  22  .
  23
  24 interpretation "Aexp plus" 'plus x y = (Add x y).
  25 interpretation "Aexp minus" 'plus x y = (Sub x y).
  26 interpretation "Aexp times" 'times x y = (Mul x y).
  27
  28 (* Boolean expressions *)
  29 inductive Bexp : Type[0] ≝
  30   | BFalse : Bexp
  31   | BTtrue : Bexp
  32   | BNot : Bexp → Bexp
  33   | BAnd : Bexp → Bexp → Bexp
  34   | BOr : Bexp → Bexp → Bexp
  35   | Eq : \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → Bexp
  36   | LE : \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → Bexp
  37 .
  38
  39 interpretation "Bexp not" 'not x = (BNot x).
  40 interpretation "Bexp and" 'and x y = (BAnd x y).
  41 interpretation "Bexp or" 'or x y = (BOr x y).
  42 interpretation "Bexp 'less or equal to'" 'leq x y = (LE x y).
  43
  44 (* Commands *)
  45 inductive Cmd : Type[0] ≝
  46   | Skip : Cmd
  47   | Assign : Var → \ 5a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"\ 6Aexp\ 5/a\ 6 → Cmd
  48   | Seq : Cmd → Cmd → Cmd
  49   | If : \ 5a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"\ 6Bexp\ 5/a\ 6 → Cmd → Cmd → Cmd
  50   | While : \ 5a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"\ 6Bexp\ 5/a\ 6 → Cmd → Cmd
  51 .
  52
  53 \ 5/pre\ 6