| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/UNITY/Comp/ (Isabelle Prover Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle README_Comp.thySprache: Isabelle |
|||||||||||||||
|
theory README_Comp imports Main begin 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
¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet am 2026-06-30) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09