We develop Stone-Kleene relation algebras, which expand Stone relation algebras with a Kleene star operation to describe reachability in weighted graphs. Many properties of the Kleene star arise as a special case of a more general theory of iteration based on Conway semirings extended by simulation axioms. This includes several theorems representing complex program transformations. We formally prove the correctness of Conway's automata-based construction of the Kleene star of a matrix. We prove numerous results useful for reasoning about weighted graphs.
We study a generalisation of relation algebras in which the underlying Boolean algebra structure is replaced with a Stone algebra. Many theorems of relation algebras generalise with no or small changes. Weighted graphs represented as matrices over extended real numbers form an instance. Relational concepts and methods can thus be applied to weighted graphs. All results are formally verified in Isabelle/HOL.
We study operations and equational properties of multirelations, which have been used for modelling games, protocols, computations, contact, closure and topology. The operations and properties are expressed using sets, heterogeneous relation algebras and more general algebras for multirelations. We investigate the algebraic properties of a new composition operation based on the correspondence to predicate transformers, different ways to express reflexive-transitive closures of multirelations, numerous equational properties, how these properties are connected and their preservation by multirelational operations. We particularly aim to generalise results and properties from up-closed multirelations to arbitrary multirelations. This paper is an extended version of .
The Internet of Things (IoT) is enabling innovative applications in various domains. Due to its heterogeneous and wide-scale structure, it introduces many new security issues. To address this problem, we propose a framework for modeling and assessing the security of the IoT and provide a formal definition of the framework. Generally, the framework consists of five phases: (1) data processing, (2) security model generation, (3) security visualization, (4) security analysis, and (5) model updates. Using the framework, we can find potential attack scenarios in the IoT, analyze the security of the IoT through well-defined security metrics, and assess the effectiveness of different defense strategies. The framework is evaluated via three scenarios, which are the smart home, wearable healthcare monitoring and environment monitoring scenarios. We use the analysis results to show the capabilities of the proposed framework for finding potential attack paths and mitigating the impact of attacks.
We develop Stone relation algebras, which generalise relation algebras by replacing the underlying Boolean algebra structure with a Stone algebra. We show that finite matrices over extended real numbers form an instance. As a consequence, relation-algebraic concepts and methods can be used for reasoning about weighted graphs. We also develop a fixpoint calculus and apply it to compare different definitions of reflexive-transitive closures in semirings.
We formally prove the correctness of Prim's algorithm for computing minimum spanning trees. We introduce new generalisations of relation algebras and Kleene algebras, in which most of the proof can be carried out. Only a small part needs additional operations, for which we introduce a new algebraic structure. We instantiate these algebras by matrices over extended reals, which model the weighted graphs used in the algorithm. Many existing results from relation algebras and Kleene algebras generalise from the relation model to the weighted-graph model with no or small changes. The overall structure of the proof uses Hoare logic. All results are formally verified in Isabelle/HOL heavily using its integrated automated theorem provers.
A range of algebras between lattices and Boolean algebras generalise the notion of a complement. We develop a hierarchy of these pseudo-complemented algebras that includes Stone algebras. Independently of this theory we study filters based on partial orders. Both theories are combined to prove Chen and Grätzer's construction theorem for Stone algebras. The latter involves extensive reasoning about algebraic structures in addition to reasoning in algebraic structures.
The notion of progress appears in various computation models, for example, in the form of traces getting longer, passing of real time, incrementing a counter, going from termination to non-termination. We introduce a model of sequential computations that generalises and abstracts these examples. We generalise existing algebras for non-terminating executions and instantiate these with our model. Using these algebras we derive an approximation order for computations with time and for trace-based computations. We introduce a generalisation of omega algebras to express iteration in the new model.
Kleene algebras with domain are Kleene algebras endowed with an operation that maps each element of the algebra to its domain of definition (or its complement) in abstract fashion. They form a simple algebraic basis for Hoare logics, dynamic logics or predicate transformer semantics. We formalise a modular hierarchy of algebras with domain and antidomain (domain complement) operations in Isabelle/HOL that ranges from domain and antidomain semigroups to modal Kleene algebras and divergence Kleene algebras. We link these algebras with models of binary relations and program traces. We include some examples from modal logics, termination and program analysis.
Multirelations have been used for modelling games, protocols and computations. They have also been used for modelling contact, closure and topology. We bring together these two lines of research using relation algebras and more general algebras. In particular, we look at various properties of multirelations that have been used in the two lines of research, show how these properties are connected and study by which multirelational operations they are preserved. We find that many results do not require a restriction to up-closed multirelations; this includes connections between various kinds of reflexive-transitive closure.
The correspondence between up-closed multirelations and isotone predicate transformers is well known. Less known is that multirelations have also been used for modelling topological contact, not only computations. We investigate how properties from these two lines of research translate to predicate transformers. To this end, we express the correspondence of multirelations and predicate transformers using relation algebras. It turns out to be similar to the correspondence between contact relations and closure operations. Many results generalise from up-closed to arbitrary multirelations.
We give axioms for an operation that describes the states from which a computation has infinite executions in several relational and matrix-based models. The models cover non-strict and strict computations which represent finite, infinite and aborting executions with varying precision. Based on the operation we provide an approximation order for a unified description of recursion. Least fixpoints in the approximation order are reduced to least and greatest fixpoints in the underlying semilattice order. We specialise this to a unified description of iteration which satisfies the axioms of a binary operation introduced in previous work. Previous consequences therefore generalise to all discussed computation models in a uniform way. All algebraic results are verified in Isabelle using its integrated automated theorem provers and SMT solvers.
We study models of state-based non-deterministic sequential computations. They differ in the kinds of computation they can represent and the precision they achieve. We systematically explore existing models, propose new models and investigate their connections. We propose algebras that describe iteration for strict and non-strict computations. They enable a unified treatment of various computation models which greatly differ in the fixpoints used to represent iteration. Our axioms are general enough to capture the semantics of while-loops in all of these models, yet powerful enough to derive complex results including program transformations and refinement theorems. We propose algebras that describe the infinite executions of a computation. In these algebras we define a unified approximation order, which applies to a wide variety of computation models. We thus obtain a unified semantics of recursion and results that connect fixpoints in the approximation and refinement orders. These results simplify reasoning about recursion and seamlessly match with our algebras for iteration when specialised to this case. We propose algebras that describe preconditions and the effect of while-programs under postconditions. Based on these we unify correctness statements in two dimensions: one statement applies in various computation models to various correctness claims. Despite their generality and the weakness of the underlying axioms we can give a sound and relatively complete correctness calculus. It also covers computation models in which choices are made by two interacting agents. The overarching algebraic method is to identify key aspects of computations, to describe these aspects by operations of algebras and to capture their properties by axioms. Theorems derived from these axioms express program transformations, correctness statements and refinement laws. We strive towards weaker axioms so as to capture more computation models. Reasoning about programs and specifications amounts to reasoning in the algebras, which can be supported by automated theorem proving technology. We extensively apply such tools to structure our results and to ensure their correctness.
This technical report contains Isabelle/HOL theories that describe algebras for iteration, infinite executions and correctness of sequential computations. The results are explained in a separate document. The Isabelle/HOL theory files are available at http://www.csse.canterbury.ac.nz/research/reports/TechReps/2015/tr_1502_theories.zip.
Previous work gives algebras for uniformly describing correctness statements and calculi in various relational and matrix-based computation models. These models support a single kind of non-determinism, which is either angelic, demonic or erratic with respect to the infinite executions of a computation. Other models, notably isotone predicate transformers or up-closed multirelations, offer both angelic and demonic choice with respect to finite executions. We propose algebras for a theory of correctness which covers these multirelational models in addition to relational and matrix-based models. Existing algebraic descriptions, in particular general refinement algebras and monotonic Boolean transformers, are instances of our theory. Our new description includes a precondition operation that instantiates to both modal diamond and modal box operators. We verify all results in Isabelle, heavily using its automated theorem provers. We integrate our theories with the Isabelle theory of monotonic Boolean transformers making our results applicable to that setting.
Conscriptions are a model of sequential computations with assumption/commitment specifications in which assumptions can refer to final states, not just to initial states. We show that they instantiate existing algebras for iteration and infinite computations. We use these algebras to derive an approximation order for conscriptions and one for extended conscriptions, which additionally represent aborting executions. We give a new computation model which generalises extended conscriptions and apply the algebraic techniques for a unified treatment.
Multirelations model computations with both angelic and demonic non-determinism. We extend multirelations to represent finite and infinite computations independently. We derive an approximation order for multirelations assuming only that the endless loop is its least element and that the lattice operations are isotone. We use relations, relation algebra and RelView for representing and calculating with multirelations and for finding the approximation order.
Extended designs distinguish non-terminating and aborting executions of sequential, non-deterministic programs. We show how to treat them algebraically based on techniques we have previously applied to total and general correctness approaches. In particular, we propose modifications to the definition of an extended design which make the theory more clear and simplify calculations, and an approximation order for recursion. We derive explicit formulas for operators on extended designs including non-deterministic choice, sequential composition, while-loops and full recursion. We show how to represent extended designs as designs or prescriptions over an extended state space. The new theory generalises our previous algebraic theory of general correctness by weakening its axioms. It also integrates with partial, total and general correctness into a common foundation which gives a unified semantics of while-programs. Program transformations derived using this semantics are valid in all four correctness approaches.
Non-strict sequential computations describe imperative programs that can be executed lazily and support infinite data structures. Based on a relational model of such computations we investigate their algebraic properties. We show that they share many laws with conventional, strict computations. We develop a common theory generalising previous algebraic descriptions of strict computation models including partial, total and general correctness and extensions thereof. Due to non-strictness, the iteration underlying loops cannot be described by a unary operation. We propose axioms that generalise the binary operation known from omega algebra, and derive properties of this new operation which hold for both strict and non-strict computations. All algebraic results are verified in Isabelle using its integrated automated theorem provers.
We give axioms for an operation that describes iteration in various relational models of computations. The models differ in their treatment of finite, infinite and aborting executions, covering partial, total and general correctness and extensions thereof. Based on the common axioms we derive separation, refinement and program transformation results hitherto known from particular models, henceforth recognised to hold in many different models. We introduce a new model that independently describes the finite, infinite and aborting executions of a computation, and axiomatise an operation that extracts the infinite executions in this model and others. From these unifying axioms we derive explicit representations for recursion and iteration. We show that also the new model is an instance of our general theory of iteration. All results are verified in Isabelle heavily using automated theorem provers.
Typed omega algebras extend Kozen's typed Kleene algebras by an operation for infinite iteration in a similar way as Cohen's omega algebras extend Kleene algebras in the untyped case. Typing these algebras is motivated by non-square matrices in automata constructions and applications in program semantics. For several reasons - the theory of untyped (Kleene or omega) algebras is well developed, results are easier to derive, and automation support is much better - it is beneficial to transfer theorems from the untyped algebras to their typed variants instead of constructing new proofs in the typed setting. Such a typing of theorems is facilitated by embedding typed algebras into their untyped variants. Extending previous work, we show that a large class of theorems of 1-free omega algebras can be transferred to typed omega algebras. This covers every universal 1-free formula which does not contain the greatest element at the beginning of an expression in a negative occurrence of an equation. Moreover, the formulas may be infinitary.
Partial, total and general correctness and further models of sequential computations differ in their treatment of finite, infinite and aborting executions. Algebras structure this diversity of models to avoid the repeated development of similar theories and to clarify their range of application. We introduce algebras that uniformly describe correctness statements, correctness calculi, pre-post specifications and loop refinement rules in five kinds of computation models. This extends previous work that unifies iteration, recursion and program transformations for some of these models. Our new description includes a relativised domain operation, which ignores parts of a computation, and represents bound functions for claims of termination by sequences of tests. We verify all results in Isabelle heavily using its automated theorem provers.
We implement a large Isabelle/HOL repository of algebras for application in modelling computing systems. They subsume computational logics such as dynamic and Hoare logics and form a basis for various software development methods. Isabelle has recently been extended by automated theorem provers and SMT solvers. We use these integrated tools for automatically proving several rather intricate refinement and termination theorems. We also automate a modal correspondence result and soundness and relative completeness proofs of propositional Hoare logic. These results show, for the first time, that Isabelle's tool integration makes automated algebraic reasoning particularly simple. This is a step towards increasing the automation of formal methods.
We investigate various fixpoint operators in a semiring-based setting that models a general correctness semantics of programs. They arise as combinations of least/greatest (pre/post) fixpoints with respect to refinement/approximation. In particular, we show isotony of these operators and give representations of fixpoints in terms of other fixpoints. Some results require completeness of the Egli-Milner order, for which we provide conditions. A new perspective is reached by exchanging the semirings with distributive lattices. They can be augmented in a natural way with a second order that is similar to the Egli-Milner order. We extend our discussion of fixpoint operators to this induced order. We show the impact on general correctness by connecting the lattice- and the semiring-based treatments to obtain results about the Egli-Milner order.
We have implemented a repository of algebraic structures and theorems in the theorem proving environment Isabelle/HOL. It covers variants of Kleene algebras and relation algebras with many of their models. Most theorems have been obtained by automated theorem proving within Isabelle. Main purposes of the repository are the engineering of algebraic theories for computing systems and their application in formal program development. This paper describes the present state of the repository, illustrates its potential by a theory engineering and a program verification example, and discusses the most important directions for future work.
We propose axioms for 1-free omega algebra, typed 1-free omega algebra and typed omega algebra. They are based on Kozen's axioms for 1-free and typed Kleene algebra and Cohen's axioms for the omega operation. In contrast to Kleene algebra, several laws of omega algebra turn into independent axioms in the typed or 1-free variants. We set up a matrix algebra over typed 1-free omega algebras by lifting the underlying structure. The algebra includes non-square matrices and care has to be taken to preserve type-correctness. The matrices can represent programs in total and general correctness. We apply the typed construction to derive the omega operation on two such representations, for which the untyped construction does not work. We embed typed 1-free omega algebra into 1-free omega algebra, and this into omega algebra. Some of our embeddings, however, do not preserve the greatest element. We obtain that the validity of a universal formula using only +, ⋅, +, ω and 0 carries over from omega algebra to its typed variant. This corresponds to Kozen's result for typed Kleene algebra.
We give an algebraic semantics of non-deterministic, sequential programs which is valid for partial, total and general correctness. It covers full recursion based on a unified approximation order. We provide explicit solutions in terms of the refinement order. As an application, we systematically derive a semantics of while-programs common to the three correctness approaches. UTP's designs and prescriptions represent programs as pairs of termination and state transition information in total and general correctness, respectively. We show that our unified semantics induces a pair-based representation which is common to the correctness approaches. Operations on the pairs, including finite and infinite iteration, can be derived systematically. We also provide the effect of full recursion on the unified, pair-based representation.
We elaborate our relational model of non-strict, imperative computations. The theory is extended to support infinite data structures. To facilitate their use in programs, we extend the programming language by concepts such as procedures, parameters, partial application, algebraic data types, pattern matching and list comprehensions. For each concept, we provide a relational semantics. Abstraction is further improved by programming patterns such as fold, unfold and divide-and-conquer. To support program reasoning, we prove laws such as fold-map fusion, otherwise known from functional programming languages. We give examples to show the use of our concepts in programs.
We integrate non-strict computations into the Unifying Theories of Programming. After showing that this is not possible with designs, we develop a new relational model representing undefinedness independently of non-termination. The relations satisfy additional healthiness conditions that model dependence in computations in an elegant algebraic form using partial orders. Programs can be executed according to the principle of lazy evaluation, otherwise known from functional programming languages. We extend the theory to support infinite data structures and give examples to show their use in programs.
We identify weak semirings, which drop the right annihilation axiom a0 = 0, as a common foundation for partial, total and general correctness. It is known how to extend weak semirings by operations for finite and infinite iteration and domain. We use the resulting weak omega algebras with domain to define a semantics of while-programs which is valid in all three correctness approaches. The unified, algebraic semantics yields program transformations at once for partial, total and general correctness. We thus give a proof of the normal form theorem for while-programs, which is a new result for general correctness and extends to programs with non-deterministic choice. By adding specific axioms to the common ones, we obtain partial, total or general correctness as a specialisation. We continue our previous investigation of axioms for general correctness. In particular, we show that a subset of these axioms is sufficient to derive a useful theory, which includes the Egli-Milner order, full recursion, correctness statements and a correctness calculus. We also show that this subset is necessary.
We generalise the designs of the Unifying Theories of Programming (UTP) by defining them as matrices over semirings with ideals. This clarifies the algebraic structure of designs and considerably simplifies reasoning about them, for example, since they form a Kleene and omega algebra and a test semiring. We apply our framework to investigate symmetric linear recursion and its relation to tail-recursion. This substantially involves Kleene and omega algebra as well as additional algebraic formulations of determinacy, invariants, domain, pre-image, convergence and Noetherity. Due to the uncovered algebraic structure of UTP designs, all our general results also directly apply to UTP.
We define a formal semantics of the combined use of UML 2 state machines, activities and interactions using Abstract State Machines. The behaviour of software models can henceforth be specified by composing these diagrams, choosing the most adequate formalism at each level of abstraction. We present several reasonable ways to link different kinds of diagrams and illustrate them by examples. We also give a formal semantics of communication between these diagrams. The resulting rules reveal unclear parts of the UML specification and serve as a basis for tool support.
General correctness offers a finer semantics of programs than partial and total correctness. We give an algebraic account continuing and extending previous approaches. In particular, we propose axioms, correctness statements, a correctness calculus, specification constructs and a loop refinement rule. The Egli-Milner order is treated algebraically and we show how to obtain least fixpoints, used to solve recursion equations, in terms of the natural order.
This is a preliminary version of .
This is a preliminary version of .
This summary of  was invited as it was short-listed for the dissertation award of the German computer science society GI.
We present a relational model of non-strict computations in an imperative, non-deterministic context. Undefinedness is represented independently of non-termination. The relations satisfy algebraic properties known from other approaches to model imperative programs; we introduce additional laws that model dependence in computations in an elegant algebraic form using partial orders. Programs can be executed according to the principle of lazy evaluation, otherwise known from functional programming languages. Local variables are treated by relational parallel composition.
Hoare and He's Unifying Theories of Programming take a relational view on semantics. The meaning of a non-deterministic, imperative program is described by 'designs' composed of two relations. They represent terminating states and relate the initial and final values of the observable variables, respectively. Several 'healthiness conditions' are imposed by the theory to obtain properties found in practice. This work determines the structure of designs and modifies the theory to support non-strict computations. It achieves these goals by identifying healthiness conditions and related axioms that involve unnecessary restrictions and subsequently removing them. The outcome provides a clear account of the algebraic foundations of the Unifying Theories of Programming. One of the results is a generalisation of designs by constructing them on semirings with ideals, structures having fewer axioms than relations. This clarifies the essential algebraic structure of designs, allows the reuse of existing mathematical theory and connects to further semantical approaches. The framework is extended by algebraic formulations of finite and infinite iteration, domain, pre-image, determinacy, invariants and convergence. Calculations and reasoning become simpler by the new, more abstract representation as is shown by applying the theory to investigate linear recursions. Another result is an extension of the Unifying Theories of Programming to deal with undefined values irrespective of non-termination. Besides being closer to practice, it forms the basis of a new theory of relations representing non-strict computations. They satisfy additional healthiness conditions that model dependence in computations in an elegant algebraic form. Programs can then be executed according to the principle of lazy evaluation, otherwise known from functional programming languages.
The token flow semantics of UML 2 activity diagrams is formally defined using Abstract State Machines. Interruptible activity regions and multiplicity bounds for pins are considered for the first time in a comprehensive and rigorous way. The formalisation provides insight into problems with the UML specification, and their solutions. It also serves as a basis for an integrated environment supporting the simulation and debugging of activity diagrams.
We generalise the designs of Unifying Theories of Programming (UTP) by defining them as matrices over semirings with ideals. This clarifies the algebraic structure of designs and considerably simplifies reasoning about them, e.g., forming a Kleene and omega algebra of designs. Moreover, we prove a generalised fixpoint theorem for isotone functions on designs. We apply our framework to investigate symmetric linear recursion and its relation to tail-recursion; this substantially involves Kleene and omega algebra as well as additional algebraic formulations of determinacy, invariants, domain, pre-image, convergence and noetherity. Due to the uncovered algebraic structure of UTP designs, all our general results also directly apply to UTP. This technical report accompanies .
We investigate the problem of finding a total order of a finite set that satisfies various local ordering constraints. Depending on the admitted constraints, we provide an efficient algorithm or prove NP-completeness. We discuss several generalisations and systematically classify the problems.
This is a preliminary version of .
We give an algebraic model of the designs of UTP based on a variant of modal semirings, hence generalising the original relational model. This is intended to exhibit more clearly the algebraic principles behind UTP and to provide deeper insight into the general properties of designs, the program and specification operators, and refinement. Moreover, we set up a formal connection with general and total correctness of programs as discussed by a number of authors. Finally we show that the designs form a left semiring and even a Kleene and omega algebra. This is used to calculate closed expressions for the least and greatest fixed-point semantics of the demonic while loop that are simpler than the ones obtained from standard UTP theory and previous algebraic approaches.
Within the Unifying Theories of Programming framework, program initiation and termination has been modelled by introducing a pair of variables in order to satisfy the required algebraic properties. We replace these variables with the improper value ⊥ that is frequently used to denote undefinedness. Both approaches are proved isomorphic using the relation calculus, and the existing operations and laws are carried over. We split the isomorphism by interposing "intuitive" relations.
This is a preliminary version of .
We investigate the problem of finding a total order of a finite set that satisfies various local ordering constraints. Depending on the admitted constraints, we provide an efficient algorithm or prove NP-completeness. To this end, we define a reduction technique and discuss its properties. This technical report accompanies .
We give an algebraic model of (H3) designs based on a variant of modal semirings, hence generalising the original relational model. This makes the theory applicable to a wider class of settings, e.g., to algebras of sets of traces. Moreover, we set up the connection with the weakly and strongly demonic semantics of programs as discussed by a number of authors. This is done using commands (a,t) where a corresponds to the transition relation of a program and the condition t characterises the input states from which termination is guaranteed. The commands form not only a semiring but even a Kleene and omega algebra. This is used to calculate closed expressions for the least and greatest fixed point semantics of the demonic while loop. This technical report accompanies .
This is a preliminary version of .
This paper describes the program transformation system Ultra. The intended use of Ultra is to assist programmers in the formal derivation of correct and efficient programs from high-level descriptive or operational specifications. We illustrate its utility by deriving a version of the Heapsort algorithm from a non-deterministic specification. Ultra supports equational reasoning about functional programs using defining equations, algebraic laws of underlying data structures, and transformation rules. The system does not only support modifying terms, but is also useful for bookkeeping and development-navigating tasks. The most salient features of Ultra are its sound theoretical foundation, its extendability, its flexible and convenient way to express transformation tasks, its comfortable user interface, and its lean and portable implementation. Ultra itself is written in the functional language Gofer.
We proceed by program transformation to derive a version of the Heapsort algorithm from a non-deterministic specification. The object language is Haskell and, therefore, the style of the resulting Heapsort program is necessarily applicative. Our development is supported by the program transformation system Ultra. Although a valuable tool, several shortcomings of Ultra are identified. This technical report accompanies .
This is a preliminary version of .
The development of correct programs is desirable for all application areas and necessary for some. In any case it is an intricate task often neglected in favour of efficiency. Compilers, which process programs to speed up their execution, are particularly sensitive. Errors can spread to all translated programs. At the same time, these profit from efficient translation results. This thesis shows the development of a correct compiler that generates efficient results. A characteristic of the logic programs translated by the compiler is that they describe problems instead of specific solution methods. The programmer can therefore focus on the actual task and better perform it. The compiler is developed by program transformation. A program is transformed stepwise into a new program that obtains the same result in a different way. This formal method requires a proof of correctness for such transitions. Particular techniques of transformation developed in this thesis can be clearly distinguished and repeatedly applied. They can be part of a strategy to develop imperative programs from functional specifications.
This manual provides an introduction to the program transformation system Ultra, sample derivations and a complete system reference. Ultra is based on a dialect of the functional programming language Haskell.
This manual describes how to organise a programming contest at a university based on experience with local competitions as part of the ACM ICPC.