4 ms·
my takeaway was modularity abstraction (as the author describes it) hides implementation and modeling abstraction reduces the system to the min. behavioral stat
by thekaranchawla 1mo ago
my takeaway was modularity abstraction (as the author describes it) hides implementation and modeling abstraction reduces the system to the min. behavioral state required to preserve your invariants
- mad44 1mo agoYes. The followup blogpost makes this more concrete over an example: https://muratbuffalo.blogspot.com/2026/08/composition-and-modular-verification-of.html https://muratbuffalo.blogspot.com/2026/08/composition-and-mo... The rely-guarantee reasoning we used in this post is where the two abstractions meet and become a joint constraint. The modularity abstraction is the boundary: we split the specs into private versus interface variables, hiding produced from the consumer and consumed from the producer. The modeling abstraction is the Env actions. E.g., EnvPut is not an API for the producer, it is a reduction of the producer: the minimal behavioral skeleton of the entire producer relevant to the consumer's property.