Reasoning about complex requirements in a uniform setting

Abstract

The paper formulates HEQ, an institution for hybrid equational logic to provide a uniform setting to express and reasoning about different sorts of properties of complex software. It is also shown how, through the definition of a suitable comorphism to FOL, this can be integrated in Hets, providing suitable tool support for teaching and re- search. The whole exercise was motivated by the need to unify, in a single undergraduate course in a Computer Science curriculum, the specification of data and behavioural constraints of reconfigurable systems.