Encoding of Circus Sample Clauses

Encoding of Circus. ‌ Semantically, Circus actions can be represented by stateful CSP processes, which we have previously integrated into Isabelle/UTP [15]. We can directly use our mechanised theory of CSP to encode Circus actions and processes. We next give some details on how this is done. Circus processes are a special kind of action where the state alphabet is empty and thus corresponds to the degenerate type unit containing only a single value. This reflects that process state is encapsulated and internal to the process, so that it cannot be seen by an environment. The key operator to define the semantics of a process is the following: The function Process takes as its argument the main action of a process over some arbitrary state ’σ, and yields an action over the unit state unit. The state hiding is carried out by the state operator, which changes the alphabet of a UTP action predicate to unit. This is achieved by first substituting the state components by some default initial values, and afterwards existentially quantifying over them. We note that the substitution step has no effect if the process initialises its state, which typically is the case. Our Circus embedding also provides a treatment of local actions. Those are encoded by a nesting of Isabelle/HOL let expressions. We hence make use of the built-in Let function of HOL for our definition of the LocalAction constructor, as it is shown below. Generally, the signature of the Let function is ’a (’a ’b) ’b for arbitrary types ’a and ’b. The constant to be locally bound (of type ’a) is supplied by the first argument. The second argument is a functional ab- straction (λ x A) in which A can refer to the local constant via the bound variable x . The semantic definition of the Let function is hence applying its second (function) argument to the value provided by the first. For convenience, Isabelle/HOL provides a custom notation for terms of the form Let c (λ x t ): they are parsed and displayed as let x = c in t , so that the user does not see the application of the Let function. We use the same technique to support the precise syntax of Circus for local actions.