theory Behaviour
imports Main
begin
datatype 'state behaviour =
Terminates 'state | Diverges | is_wrong: Goes_wrong 'state
text ‹
behaviours are annotated with the last state of the execution in order to compare the result of two executions with the @{const rel_behaviour} relation.
exact meaning of the three behaviours is defined in the semantics locale
›
end
¤ Dauer der Verarbeitung: 0.2 Sekunden
¤
*© Formatika GbR, Deutschland
