Xxxxxxxx/UTP. In order to verify the correctness of UTP-based semantic models, we need mechanical support for formalising UTP theories, proving algebraic laws, composing them to produce denota- tional models, and providing provably corresponding semantic bases. In a theorem prover like Xxxxxxxx, we can go even further and construct proof tactics and procedures for proving prop- erties of theory objects (i.e. programs or models) in a particular semantic interface, such as a Hoare logic based program verifier. This then means that we have an unbroken chain from proof of program correctness to justification in terms of high-level properties in the underlying denotational semantic models and theories. We have therefore mechanised the UTP semantic framework in Isabelle/UTP [15, 17]. Is- abelle/UTP is a framework that allows the formation of theories, semi-automated proof of their properties, and theory combination to provide semantic models. It is a (relatively) deep se- mantic embedding of the UTP relational calculus into the HOL object logic. Unlike typical deep embeddings, it is also integrated with Xxxxxxxx’s type system and automated proof tactics. Thus it allows both precise reasoning about program semantics, and also facilitates program verification. Xxxxxxxx/UTP facilitates mechanised theory engineering, that is the creation and false ▶ Q = ⊥D (8) ⊥D; (P ▶ Q) = ⊥D (9) (P1 ▶ Q1) H (P2 ▶ Q2) = (P1 ∧ P2 ▶ Q1 ∨ Q2) (10) (p1 ▶ Q1); (p2 ▶ Q2) = (p1 ∧ (Q1 wp p2)) ▶ (Q1; Q2) (11) Table 5: Algebraic laws of designs Figure 2: A UTP proof using the ISAR language exploration of the theories of programming with machine aided reasoning facilities. For exam- ple, all the laws shown in Tables 3 and 5 have been verified with respect to our model in this framework. We give a model to alphabetised predicates as a derived Isabelle type, and then define the standard constructs of predicates and relations as Isabelle functions. We also give a purely se- mantic model to expressions, variable renaming, and substitution. We then define proof tactics that allow us to automate proofs. The majority of these tactics work by soundly translating a UTP predicate into some kind of Xxxxxxxx/HOL construct, such as sets or binary relations, for which a large number of laws have already been proven. For example utp-pred-tac converts a UTP predicate into a HOL predicate, and this allow standard predicate reasoning to be applied. In contrast utp-rel-tac can be applied to relational conjecture, through ...
