In his book A practical theory of programming [10] , [12] , Eric Hehner proposes and applies a radical reformulation of set theory in which the collection and packaging of elements are seen as separate activities. This provides for unpackaged collections, referred to as “bunches”. Bunches allow us to reason about non-determinism at the level of terms, and, very remarkably, allow us to reason about the conceptual entity “nothing”, which is just an empty bunch (and very different from an empty set). This eliminates mathematical “gaps” caused by undefined terms. We have made use of bunches in a number of papers that develop a refinement calculus for backtracking programs. We formulate our bunch theory as an extension of the set theory used in the B-Method, and provide a denotational model to give this formulation a sound mathematical basis. We replace the classical logic that underpins B with a version that is still able to prove the laws of our logic toolkit, but is unable to prove the property, derivable in classical logic, that every term denotes an element, which for us is pathological since we hold that terms such as 1/0 simply denote “nothing”. This change facilitates our ability to reason about partial functions and backtracking programs. We include a section on our backtracking program calculus, showing how it is derived from WP and how bunch theory simplifies its formulation. We illustrate its use with two small case studies .

Neurofeedback systems can be modeled as closed-loop control systems with negative feedback. However, little work to date has investigated the potential of this representation in gaining a better understanding of the actual dynamics of neurofeedback towards explaining subjects' performance. In this paper, we analyze neurofeedback training data through a PID control model. We first show that PID model fitting can produce curves that are qualitatively aligned to the measured BCI signal. Secondly, we examine how brain activity during neurofeedback can be related to common characteristics of control systems. For this, we formalized a pre-existing neurofeedback EEG experiment using a Simulink®model that captures both the neural activity and the external algorithm that was utilized to generate the feedback signal. We then used a regression model to fit individual trial data to PID coefficients for the control model. Our results suggest that successful trials tend to be associated to higher average values of Ki, which represents the error-reducing component of the PID controller. It hints that convergence in successful neurofeedback is progressive but complete in approaching the target.

Abstract Safety-Critical Java (SCJ) is a recent technology that changes the execution and memory model of Java in such a way that applications can be statically analysed and certified for their real-time properties and safe use of memory. Our interest is in the development of comprehensive and sound techniques for the formal specification, refinement, design, and implementation of SCJ programs, using a correct-by-construction approach. As part of this work, we present here an account of laws and patterns that are of general use for the refinement of SCJ mission specifications into designs of parallel handlers, as they are used in the SCJ programming paradigm. Our refinement notation is a combination of languages from theCircusfamily, supporting state-rich reactive models with the addition of class objects and real-time properties. Starting from a sequential and centralisedCircusspecification, our laws permit refinement intoCircusmodels of SCJ program designs. Automation and proof of the refinement laws is examined here, too. Our work is an important step towards eliciting laws of programming for SCJ and fits into a refinement strategy that we have developed previously to derive SCJ programs from specifications in a rigorous manner.

Safety-critical Java (SCJ) is a restriction of the real-time specification for Java to support the development and certification of safety-critical applications. The SCJ technology specification is the result of an international effort from industry and academia. In this paper, we present a formalization of the SCJ Level 1 execution model, formalize a translation strategy from SCJ into a refinement notation and describe a tool that largely automates the generation of the formal models. Our modelling language is part of the Circus family; at the core, we have Z, communicating sequential processes and Morgan's calculus, but we also use object-oriented and timed constructs from the OhCircus and Circus Time variants. Our work is an essential ingredient for the development of refinement-based reasoning techniques for SCJ.

Abstract We see reversible computing as a generalisation of sequential computation obtained by revoking the law of the excluded miracle. Our execution language includes naked guarded commands and non-deterministic choice. Choices which lead to miraculous continuations invoke reverse computation, and non-deterministic choice plays the rôle of provisional choice within a backtracking context. We require probabilistic choice for symmetry breaking and sampling large search spaces, but must formulate it differently from previous approaches to obtain the required interactions between probabilistic choice and non-deterministic choice and between probabilistic choice and feasibility. Our formulation allows us to derive the post-distributions which characterise a program, and we use these to construct a relational model. We consider refinement as containment of convex closures within distribution space, qualified with additional conditions to avoid over-refinement. We link the non-probabilistic and probabilistic versions of the model with a Galois connection and show that classical designs are a retract of our probabilistic designs. We consider the interaction between probabilistic and non-deterministic choice and find the same initially counter-intuitive results that have been noted by other investigators. We provide an alternative formulation, within the same model, of oblivious non-determinism, which allows all non-deterministic choices to be moved to the start of a computation. We consider the interaction between probabilistic choice and feasibility that is required to match an operational interpretation in which infeasible commands provoke reverse execution, and we present a small case study to show how the interaction between probabilistic choice and feasibility can be exploited in a practical program. All programming structures described here are supported by our implementation platform, the Reversible Virtual Machine, whose development has accompanied our theoretical investigations.

Abstract ArcAngel is a tactic language devised to facilitate and automate program developments using Morgan’s refinement calculus. It is especially well suited for the specification of high-level refinement strategies, and equipped with a formal semantics that additionally permits reasoning about tactics. In this paper, we present an implementation of ArcAngel for the ProofPower theorem prover. We discuss the underlying design, explain how it implements the semantics of ArcAngel, and examine the interplay between ArcAngel tactics and the native reasoning support of the prover. We also discuss several extensions of ArcAngel that have been entailed by our implementation effort. They are of practical importance and provide a unification of the related tactic languages Angel and ArcAngelC. Our main result is a mechanisation that reflects directly the ArcAngel semantics, and can be used with any programming model for refinement. The approach can be used to support other formal tactic languages using other theorem provers.