tcs3.cspcasl revision 567db7182e691cce5816365d8c912d09ffe92f86
4df55fde49134f9735f84011f23a767c75e393c7Janie Luccspec tcs3 =
4df55fde49134f9735f84011f23a767c75e393c7Janie Ludata sorts S, T
4df55fde49134f9735f84011f23a767c75e393c7Janie Lu ops f: S ->? T
4df55fde49134f9735f84011f23a767c75e393c7Janie Lu . forall x: S . not def f(x)
4df55fde49134f9735f84011f23a767c75e393c7Janie Luprocess (?x: S -> f(x) -> SKIP) [| T |] (?y : T -> if def y then SKIP else STOP)