The semantics of a little programming language is described with the following declarations :

Require Export ZArith. Ltac CaseEq f := Generalize (refl_equal f); Pattern -1 f; Case f. Section little_abstract_semantics. Variables (Var, aExp, bExp, state : Set) (evalA : state -> aExp -> option Z) (evalB : state -> bExp -> option bool) (update : state -> Var -> Z -> option state). Inductive inst : Set := Skip: inst | Assign: Var -> aExp -> inst | Scolon: inst -> inst -> inst | WhileDo: bExp -> inst -> inst . Implicits Some [1]. (* The semantics of the language is given in chapter 7. *) Inductive exec : state -> inst -> state -> Prop := execSkip: forall s : state, exec s Skip s | execAssign: forall (s s1 : state) (v : Var) (n : Z) (a : aExp), evalA s a = Some n -> update s v n = Some s1 -> exec s (Assign v a) s1 | execScolon: forall (s s1 s2 : state) (i1 i2 : inst), exec s i1 s1 -> exec s1 i2 s2 -> exec s (Scolon i1 i2) s2 | execWhileFalse: forall (s : state) (i : inst) (e : bExp), evalB s e = Some false -> exec s (WhileDo e i) s | execWhileTrue: forall (s s1 s2 : state) (i : inst) (e : bExp), evalB s e = Some true -> exec s i s1 -> exec s1 (WhileDo e i) s2 -> exec s (WhileDo e i) s2.

We use the predicate `forLoops` to characterize a subset of programs
for which execution is guaranteed to terminate (if there are no execution errors).

(* We need to use the evaluation functions as if they were total. extract_optio n makes them total by adding a default value. *) Definition extract_option : forall A : Set, option A -> A -> A := fun A x def => match x with None => def | Some v => v end. Implicits extract_option [1]. (* When a while loop contains a variable that is decreased at each step and tested against a bound, it is obvious that this loop will terminate. We consider such loops are "for" loops.*) Inductive forLoops : inst -> Prop := aForLoop: forall (e : bExp) (i : inst) (variant : aExp), (forall s, s' : state, evalB s e = Some true -> exec s i s' -> Zwf ZERO (extract_option (evalA s' variant) ZERO) (extract_option (evalA s variant) ZERO)) -> forLoops i -> forLoops (WhileDo e i) | assignFor: forall (v : Var) (e : aExp), forLoops (Assign v e) | skipFor: forLoops Skip | scolonFor: forall i1 i2 : inst, forLoops i1 -> forLoops i2 -> forLoops (Scolon i1 i2).

Define a function with the following type :

forall (s : state) (i : inst), forLoops i -> {s' : state | exec s i s'}+{forall s' : state, ~ exec s i s'}.

Here is a hint: look at the files from the Coq standard library where
`well-founded` appears.

Going home

Yves Bertot Last modified: Wed May 7 01:42:58 MEST 2003