Verifiable and Executable Logic Specifications of Concurrent Objects in L_pi
Luı́s Caires, Luis Fraser Monteiro · 1998
We present the core-L_pi fragment of L_pi and its program logic. We illustrate the adequacy of L_pi as a meta-language for jointly defining operational semantics and program logics of languages with concurrent and logic features, considering the case of a specification logic for concurrent objects addressing mobile features like creation of objects and channels in a simple way. Specifications are executable by a translation that assigns to every specification a model in the form of a core-L_pi program. We also illustrate the usefulness of this framework in reasoning about systems and their components.