SSL RG_Com.thy
Interaktion und PortierbarkeitIsabelle
chapter‹The Rely-Guarantee Method›
section‹Abstract Syntax›
theory RG_Com imports Main begin
text‹Semantics of assertions and boolean expressions (bexp) as sets
states. Syntax of commands ‹com› and parallel commands ‹par_com›.›
type_synonym 'a bexp = "'a set"
datatype 'a com =
Basic "'a →'a"
| Seq "'a com""'a com"
| Cond "'a bexp""'a com""'a com"
| While "'a bexp""'a com"
| Await "'a bexp""'a com"
type_synonym 'a par_com = "'a com option list"
end
Messung V0.5 in Prozent
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.10Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-09-29)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
