section‹UNITY: Examples Involving Program Composition›
text‹
The directory presents verification examples involving program composition.
They are mostly taken from the works of Chandy, Charpentier and Chandy.
▪ examples of ∗‹universal properties›: the counter (🚫‹Counter.thy›) and
priority system (🚫‹Priority.thy›) ▪ the allocation system (🚫‹Alloc.thy›) ▪ client implementation (🚫‹Client.thy›) ▪ allocator implementation (🚫‹AllocImpl.thy›) ▪ the handshake protocol (🚫‹Handshake.thy›) ▪ the timer array (demonstrates arrays of processes) (🚫‹TimerArray.thy›)
Safety proofs (invariants) are often proved automatically. Progress proofs
involving ENSURES can sometimes be proved automatically. The level of
automation appears to be about the same as in HOL-UNITY by Flemming Andersen
et al. ›
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet am 2026-06-30)
¤
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.
