Unifying theories of logic and specification

Abstract

We propose a unifying treatment of multi-valued logic in the general context of specification, presented in the style of the Unifying Theories of Programming of Hoare and He. At a low level, UTP theories correspond to different types of three-valued logic. At higher levels they correspond to individual specifications. Designs are considered as their models, but members of other unifying theories of computation can serve as models just as well. Using this setup we have the opportunity to show correspondences between specification languages that use different logics. © 2013 Springer-Verlag.