The Semantics of Mojave
This chapter presents a Hoare-style programming logic for Mojave. Based on this axiomatic semantics, we prove interesting language properties such as type safety. Moreover, we present a definition of modular correctness and discuss modular soundness. The chapter concludes with a discussion of related work.
KeywordsProgramming Logic Open Program Proof Obligation Constant Symbol Dynamic Type
Unable to display preview. Download preview PDF.