Home

Module Events


Representation of observable events and execution traces.

The observable behaviour of programs is stated in terms of input/output events, which can also be thought of as system calls to the operating system. An event is generated each time an external function (see module AST) is invoked. The event records the name of the external function, the arguments to the function invocation provided by the program, and the return value provided by the outside world (e.g. the operating system). Arguments and values are either integers or floating-point numbers. We currently do not allow pointers to be exchanged between the program and the outside world.

Load Param.

Record tr : Type := make_tr {
  trace : Type;
  E0 : trace;
  Eapp : trace -> trace -> trace;
  traceinf : Type;
  Eappinf : trace -> traceinf -> traceinf;
  outcome : Type
}.

Concatenation of traces is written ** in the finite case or *** in the infinite case.
Infix "**" := Eapp (at level 60, right associativity).
Infix "***" := Eappinf (at level 60, right associativity).
Implicit Arguments E0 [t].

Record trsem (t0 : tr) : Prop := trsem_intro {
  E0_left: forall t : _ t0, E0 ** t = t;
  E0_right: forall t : _ t0, t ** E0 = t;
  Eapp_assoc: forall t1 t2 t3 : _ t0, (t1 ** t2) ** t3 = t1 ** (t2 ** t3);
  Eapp_E0_inv: forall t1 t2 : _ t0, t1 ** t2 = E0 -> t1 = E0 /\ t2 = E0;
  E0_left_inf: forall T : _ t0, E0 *** T = T;
  Eappinf_assoc: forall (t1 t2 : _ t0) T, (t1 ** t2) *** T = t1 *** (t2 *** T)
}.

Hint Rewrite E0_left E0_right Eapp_assoc
             E0_left_inf Eappinf_assoc: trace_rewrite.