Many programs are executed according to the conventional, eager execution order, for which verification of execution costs is well-understood. However, there are other execution orders in use. One such order in common use is lazy execution or lazy evaluation, which is mostly demand-driven. Laziness supports better decompositions of algorithms, e.g., into modular producers and consumers, which enables compositional reasoning of answer correctness, but then timing correctness is more elusive. This thesis gives a formal method for verifying lazy timing, compositional with respect to program structure; it is an extension of a predicative programming theory. Predicative programming theories are formal methods that unify both specifications and programs as predicates or boolean-typed expressions over memory state and other quantities of interest. Their strengths are mathematical simplicity and support of program development and verification by incremental refinements. Among these theories, Hehner's a Practical Theory of Programming has the further strength of leaving termination and timing open rather than a built-in, and therefore is a flexible substrate for various timing schemes corresponding to various execution strategies. We use this substrate for our method for lazy timing. This thesis also proves soundness of the eager timing scheme in Hehner's work with respect to an eager operational semantics, and our lazy timing scheme with respect to a lazy operational semantics. Thus, if refinements promise an upper time bound, then execution actually stops within that time. Lastly, this thesis outlines a space of more operational semantics. It is possible ground for more execution strategies.

Many programs are executed according to the conventional, eager execution order, for which verification of execution costs is well-understood. However, there are other execution orders in use. One such order in common use is lazy execution or lazy evaluation, which is mostly demand-driven. Laziness supports better decompositions of algorithms, e.g., into modular producers and consumers, which enables compositional reasoning of answer correctness, but then timing correctness is more elusive. This thesis gives a formal method for verifying lazy timing, compositional with respect to program structure; it is an extension of a predicative programming theory. Predicative programming theories are formal methods that unify both specifications and programs as predicates or boolean-typed expressions over memory state and other quantities of interest. Their strengths are mathematical simplicity and support of program development and verification by incremental refinements. Among these theories, Hehner's a Practical Theory of Programming has the further strength of leaving termination and timing open rather than a built-in, and therefore is a flexible substrate for various timing schemes corresponding to various execution strategies. We use this substrate for our method for lazy timing. This thesis also proves soundness of the eager timing scheme in Hehner's work with respect to an eager operational semantics, and our lazy timing scheme with respect to a lazy operational semantics. Thus, if refinements promise an upper time bound, then execution actually stops within that time. Lastly, this thesis outlines a space of more operational semantics. It is possible ground for more execution strategies.

Hoare and He's Unifying Theories of Programming (UTP) provides a rich model of programs as relational predicates. This theory is intended to provide a single framework in which any programming paradigms, languages, and features, can be modelled, compared and contrasted. The UTP already has models for several programming formalisms, such as imperative programming, higher-order programming (e.g. programing with procedures), several styles of concurrent programming (or reactive systems), class-based object-orientation, and transaction processing. We believe that the UTP ought to be able to represent all significant computer programming language formalisms, in order for it to be considered a unifying theory. One gap in the UTP work is that of object-based object-orientation, such as that presented in Abadi and Cardelli's untyped object calculi (sigma-calculi). These sigma-calculi provide a prominent formalism of object-based object-oriented (OO) programs, which models programs as objects. We address this gap within this dissertation by presenting an embedding of an Abadi--Cardelli-style object calculus in the UTP. More formally, the thesis that his dissertation argues is that it is possible to provide an object-based object rientation to the UTP, with value- and reference-based objects, and a fully abstract model of references. We have made three contributions to our area of study: first, to extend the UTP with a notion of object-based object orientation, in contrast with the existing class-based models; second, to provide an alternative model of pointers (references) for the UTP that supports both value-based compound values (e.g. objects) and references (pointers), in contrast to existing UTP models with pointers that have reference-based compound values; and third, to model an Abadi-Cardelli notion of an object in the UTP, and thus demonstrate that it can unify this style of object formalism.