The approach to reasoning about structural operational semantics style specifications supported by the Abella system is discussed. This approach uses lambda tree syntax to treat object language binding and encodes binding related properties in generic judgments. Further, object language specifications are embedded directly into the reasoning framework through recursive definitions. The treatment of binding via generic judgments implicitly enforces distinctness and atomicity in the names used for bound variables. These properties must, however, be made explicit in reasoning tasks. This objective can be achieved by allowing recursive definitions to also specify generic properties of atomic predicates. The utility of these various logical features in the Abella system is demonstrated through actual reasoning tasks. Brief comparisons with a few other logic based approaches are also made.
Abella is an interactive system for reasoning about aspects of object languages that have been formally presented through recursive rules based on syntactic structure. Abella utilizes a two-level logic approach to specification and reasoning. One level is defined by a specification logic which supports a transparent encoding of structural semantics rules and also enables their execution. The second level, called the reasoning logic, embeds the specification logic and allows the development of proofs of properties about specifications. An important characteristic of both logics is that they exp…
The Abella interactive theorem prover has proven to be an effective vehicle for reasoning about relational specifications. However, the system has a limitation that arises from the fact that it is based on a simply typed logic: formalizations that are identical except in the respect that they apply to different types have to be repeated at each type. We develop an approach that overcomes this limitation while preserving the logical underpinnings of the system. In this approach object constructors, formulas and other relevant logical notions are allowed to be parameterized by types, with the in…
In logical reasoning, it is often the case that only some of a collection of assumptions are needed to reach a conclusion. A strengthening lemma is an assertion that a given conclusion is independent in this sense of a particular assumption. Strengthening lemmas underlie many useful techniques for simplifying proofs in automated and interactive theorem-provers. For example, they underlie a mechanism called subordination that is useful in determining that expressions of a particular type cannot contain objects of another type and in thereby reducing the number of cases to be considered in provi…
The logic of hereditary Harrop formulas (HH) has proven useful for specifying a wide range of formal systems. This logic includes a form of hypothetical judgment that leads to dynamically changing sets of assumptions and that is key to encoding side conditions and contexts that occur frequently in structural operational semantics (SOS) style presentations. Specifications are often useful in reasoning about the systems they describe. The Abella theorem prover supports such reasoning by explicitly embedding the specification logic within a rich reasoning logic; specifications are then reasoned a…
This thesis concerns the development of a framework that facilitates the design and analysis of formal systems. Specifically, this framework provides a specification language which supports the concise and direct description of formal systems, a mechanism for animating the specification language thereby producing prototypes of encoded systems, and a logic for proving properties of specifications and therefore of the systems they encode. A defining characteristic of the proposed framework is that it is based on two separate but closely intertwined logics: a specification logic that facilitates …
Relational descriptions have been used in formalizing diverse computational notions, including, for example, operational semantics, typing, and acceptance by non-deterministic machines. We therefore propose a (restricted) logical theory over relations as a language for specifying such notions. Our specification logic is further characterized by an ability to explicitly treat binding in object languages. Once such a logic is fixed, a natural next question is how we might prove theorems about specifications written in it. We propose to use a second logic, called a reasoning logic, for this purpo…
We argue that the implementation and verification of compilers for functional programming languages are greatly simplified by employing a higher-order representation of syntax known as Higher-Order Abstract Syntax or HOAS. The underlying idea of HOAS is to use a meta-language that provides a built-in and logical treatment of binding related notions. By embedding the meta-language within a larger programming or reasoning framework, it is possible to absorb the treatment of binding structure in the object language into the meta-theory of the system, thereby greatly simplifying the overall implem…
Structural operational semantics (SOS) is a technique for defining operational semantics for programming and specification languages. Because of its intuitive appeal and flexibility, SOS has found considerable application in the study of the semantics of concurrent processes. It is also a viable alternative to denotational semantics in the static analysis of programs and in proving compiler correctness. Recently it has been applied in emerging areas such as probabilistic systems and systems biology.
This volume contains the proceedings of SOS 2009, the Sixth Workshop on Structural Operational Semantics held on the 31st of August 2009 in Bologna, Italy as a affiliated workshop of CONCUR 2009, the 20th International Conference on Concurrency Theory. Structural operational semantics (SOS) is a technique for defining operational semantics for programming and specification languages. The workshop is forum for researchers, students and practitioners interested in new developments and directions for future investigations in the area of SOS. One of the specific goals of the workshop is to provide…
We give a leisurely introduction to our abstract framework for operational semantics based on cellular monads on transition categories. Furthermore, we relate it for the first time to an existing format, by showing that all Positive GSOS specifications generate cellular monads whose free algebras are all compositional. As a consequence, we recover the known result that bisimilarity is a congruence in the generated labelled transition system.
We present a concurrent operational Petri net semantics for the join-calculus, a process calculus for specifying concurrent and distributed systems. There often is a gap between system specifications and the actual implementations caused by synchrony assumptions on the specification side and asynchronously interacting components in implementations. The join-calculus is promising to reduce this gap by providing an abstract specification language which is asynchronously distributable. Classical process semantics establish an implicit order of actually independent actions, by means of an interlea…
Snapshot isolation (SI) is a standard transactional consistency model used in databases, distributed systems and software transactional memory (STM). Its semantics is formally defined both declaratively as an acyclicity axiom, and operationally as a concurrent algorithm with memory bearing timestamps. We develop two simpler equivalent operational definitions of SI as lock-based reference implementations that do not use timestamps. Our first locking implementation is prescient in that requires a priori knowledge of the data accessed by a transaction and carries out transactional writes eagerly …
General frameworks have been recently proposed as unifying theories for processes combining non-determinism with quantitative aspects (such as probabilistic or stochastically timed executions), aiming to provide general results and tools. This paper provides two contributions in this respect. First, we present a general GSOS specification format and a corresponding notion of bisimulation for non-deterministic processes with quantitative aspects. These specifications define labelled transition systems according to the ULTraS model, an extension of the usual LTSs where the transition relation as…
This thesis deals with the specification and construction of syntax and operational semantics of a programming language. We work with a general notion of signature for specifying objects of a given category as initial objects in a suitable category of models.This characterization, in the spirit of Initial Semantics, gives a justification of the recursion principle. Languages with variable binding, such as the pure lambda calculus, are monads on the category of sets specified through the classical algebraic signatures. The first extensions to syntaxes with equations that we consider are quotien…
We propose $\mathcal{E}^{\downarrow}$-logic as a formal foundation for the specification and development of event-based systems with local data states. The logic is intended to cover a broad range of abstraction levels from abstract requirements specifications up to constructive specifications. Our logic uses diamond and box modalities over structured actions adopted from dynamic logic. Atomic actions are pairs $e /ψ$ where $e$ is an event and $ψ$ a state transition predicate capturing the allowed reactions to the event. To write concrete specifications of recursive process structures we integ…
This volume contains the proceedings of SOS 2011, the Eight Workshop on Structural Operational Semantics, held on the 5th of September 2011 in Aachen, Germany as an affiliated workshop of CONCUR 2011, the 22nd International Conference on Concurrency Theory. Structural operational semantics (SOS) provides a framework for giving operational semantics to programming and specification languages. A growing number of programming languages from commercial and academic spheres have been given usable semantic descriptions by means of structural operational semantics. Because of its intuitive appeal and…
This paper presents an example of formal reasoning about the semantics of a Prolog program of practical importance (the SAT solver of Howe and King). The program is treated as a definite clause logic program with added control. The logic program is constructed by means of stepwise refinement, hand in hand with its correctness and completeness proofs. The proofs are declarative - they do not refer to any operational semantics. Each step of the logic program construction follows a systematic approach to constructing programs which are provably correct and complete. We also prove that correctness…
This paper presents an operational semantics for UML activity diagrams. The purpose of this semantics is three-fold: to give a robust basis for verifying model correctness; to help validate model transformations; and to provide a well-formed basis for assessing whether a proposed extension/interpretation of the modeling language is consistent with the standard. The challenges of a general formal framework for UML models include the semi-formality of the semantics specification, the extensibility of the language, and (sometimes deliberate, sometimes accidental) under-specification of model beha…
This volume contains the proceedings of the Combined 21st International Workshop on Expressiveness in Concurrency and the 11th Workshop on Structural Operational Semantics (EXPRESS/SOS 2014) which was held on 1st September 2014 in Rome, Italy, as an affiliated workshop of CONCUR 2014, the 25th International Conference on Concurrency Theory. The EXPRESS workshops aim at bringing together researchers interested in the expressiveness of various formal systems and semantic notions, particularly in the field of concurrency. Their focus has traditionally been on the comparison between programming co…
This volume contains the proceedings of the Combined 20th International Workshop on Expressiveness in Concurrency and the 10th Workshop on Structural Operational Semantics (EXPRESS/SOS 2013) which was held on 26th August, 2013 in Buenos Aires, Argentina, as an affiliated workshop of CONCUR 2013, the 24th International Conference on Concurrency Theory. The EXPRESS workshops aim at bringing together researchers interested in the expressiveness of various formal systems and semantic notions, particularly in the field of concurrency. Their focus has traditionally been on the comparison between pro…
Runtime verification (RV) consists in dynamically verifying that the event traces generated by single runs of a system under scrutiny (SUS) are compliant with the formal specification of its expected properties. RML (Runtime Monitoring Language) is a simple but expressive Domain Specific Language for RV; its semantics is based on a trace calculus formalized by a deterministic rewriting system which drives the implementation of the interpreter of the monitors generated by the RML compiler from the specifications. While determinism of the trace calculus ensures better performances of the generat…
Runtime verification (RV) consists in dynamically verifying that the event traces generated by single runs of a system under scrutiny (SUS) are compliant with the formal specification of its expected properties. RML (Runtime Monitoring Language) is a simple but expressive Domain Specific Language for RV; its semantics is based on a trace calculus formalized by a deterministic rewriting system which drives the implementation of the interpreter of the monitors generated by the RML compiler from the specifications. While determinism of the trace calculus ensures better performances of the generat…
Thom Frühwirth presented a short, elegant and efficient Prolog program for the n queens problem. However the program may be seen as rather tricky and one may be not convinced about its correctness. This paper explains the program in a declarative way, and provides proofs of its correctness and completeness. The specification and the proofs are declarative, i.e. they abstract from any operational semantics. The specification is approximate, it is unnecessary to describe the program's semantics exactly. Despite the program works on non-ground terms, this work employs the standard semantics, base…
Creol is an object-oriented modeling language in which inherently concurrent objects exchange asynchronous method calls. The operational semantics of Creol is written in an actor-based style, formulated in rewriting logic. The operational semantics yields a language interpreter in the Maude system, which can be used to analyze models. Recently, Creol has been applied to the modeling of systems with radio communication, such as sensor systems. With radio communication, messages expire and, if sent simultaneously, they may collide in the air. In order to capture these and other properties of dis…
This paper addresses the issue of specifying, simulating, and verifying reactive systems in rewriting logic. It presents an executable semantics for probabilistic, timed, and spatial concurrent constraint programming -- here called stochastic and spatial concurrent constraint systems (SSCC) -- in the rewriting logic semantic framework. The approach is based on an enhanced and generalized model of concurrent constraint programming (CCP) where computational hierarchical spaces can be assigned to belong to agents. The executable semantics faithfully represents and operationally captures the highl…
Thom Frühwirth presented a short, elegant and efficient Prolog program for the n queens problem. However the program may be seen as rather tricky and one may not be convinced about its correctness. This paper explains the program in a declarative way, and provides proofs of its correctness and completeness. The specification and the proofs are declarative, i.e. they abstract from any operational semantics. The specification is approximate, it is unnecessary to describe the program's semantics exactly. Despite the program works on non-ground terms, this work employs the standard semantics, base…
Modern processors deploy a variety of weak memory models, which for efficiency reasons may execute instructions in an order different to that specified by the program text. The consequences of instruction reordering can be complex and subtle, and can impact on ensuring correctness. In this paper we build on extensive work elucidating the semantics of assembler-level languages on hardware architectures with weak memory models (specifically TSO, ARM and POWER) and lift the principles to a straightforward operational semantics which allows reasoning at a higher level of abstraction. To this end w…
Computational psychology has the aim to explain human cognition by computational models of cognitive processes. The cognitive architecture ACT-R is popular to develop such models. Although ACT-R has a well-defined psychological theory and has been used to explain many cognitive processes, there are two problems that make it hard to reason formally about its cognitive models: First, ACT-R lacks a formalization of its underlying production rule system and secondly, there are many different implementations and extensions of ACT-R with technical artifacts complicating formal reasoning even more. T…
In this paper I distinguish two (pre)congruence requirements for semantic equivalences and preorders on processes given as closed terms in a system description language with a recursion construct. A lean congruence preserves equivalence when replacing closed subexpressions of a process by equivalent alternatives. A full congruence moreover allows replacement within a recursive specification of subexpressions that may contain recursion variables bound outside of these subexpressions. I establish that bisimilarity is a lean (pre)congruence for recursion for all languages with a structural operat…
