f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblettlogic CspCASL

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblettspec tcs3 =

4eaeba586d49aa0761ee2bb6d20efba91562cef6Andy Gimblettdata sorts S, T

4eaeba586d49aa0761ee2bb6d20efba91562cef6Andy Gimblett ops f: S ->? T

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett . forall x: S . not def f(x);

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblettprocess

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett (?x: S -> f(x) -> SKIP) [| T |] (?y : T -> (if def y then SKIP else STOP))