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.0 Sekunden
(vorverarbeitet am 2026-05-03)
¤
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.
