Cooperative Specification via Composition Control
summary
Proposes concrete language extensions for Datalog, Alloy and eFLINT that let contributors declare how fragments may be composed and changed, turning meta‑level policies into checkable rules. Demonstrations show a static control that rejects illegal edits by syntactic inspection (catching violations before model search) and a contributor‑tracking dynamic check that flags inferred facts whose provenance mismatches the allowed author, plus a P1–P2–P3 control triple pattern for intercepting harmful later additions. Uses the Alloy analyzer and eFLINT examples; shows when unsat vs valid hides root causes.
AI-written summary · about
chapters (17)
- 0:00Cooperative specification intro
- 1:04Motivation
- 2:54Running example
- 5:45Limitations
- 7:08Spec language requirements
- 8:16Composition control concept
- 9:01Static composition in Eelin
- 11:30Dynamic composition in Eelin
- 14:19Control triple pattern
- 16:26Access modifiers comparison
- 16:46Composition control in Alloy
- 19:55Alloy unsatisfiable constraints
- 21:40Alloy static constraints
- 22:40Paper contributions
- 23:45Future directions
- 24:06Multi-agent integration
- 24:48Q&A
related talks
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
39mCompositional protocol (..) communicating actors
23mSpecifying and Verifying Future Conditions
20mA Modular Approach to Metatheoretic Reasoning for Extensible Languages
36mSpecification-Guided Component-Based Synthesis from Effectful Libraries
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
19mLanguage Support for Refactorability Decay Prevention
16mA metalanguage for multi-phase modularity