6ae232055d4d8a97267517c5e50074c2c819941andlogic CspCASL

6ae232055d4d8a97267517c5e50074c2c819941andspec tcs3 =

6ae232055d4d8a97267517c5e50074c2c819941anddata sorts S, T

6ae232055d4d8a97267517c5e50074c2c819941and ops f: S ->? T

6ae232055d4d8a97267517c5e50074c2c819941and . forall x: S . not def f(x);

6ae232055d4d8a97267517c5e50074c2c819941andprocess

6ae232055d4d8a97267517c5e50074c2c819941and tcs3: S, T;

6ae232055d4d8a97267517c5e50074c2c819941and tcs3 = [] x :: S -> f(x) -> SKIP

6ae232055d4d8a97267517c5e50074c2c819941and [| T |]

6ae232055d4d8a97267517c5e50074c2c819941and [] y :: T -> (if def y then SKIP else STOP)

6ae232055d4d8a97267517c5e50074c2c819941and