Example using a network model. It is meant to illustrate the use of abstract trace specifications, as well as the possibility of having different implementations for such a specification, depending on a chosen network semantics.
This example appears in the ESOP'2022 paper "Why3-do: The Way of Harmonious Distributed System Proofs".
- specLDT.mlw: abstract (trace-based) specification of lock
- LDT.mlw: implementation of lock assuming idealized network semantics
- LDTDupl.mlw: implementation of lock assuming packet-duplicating semantics