Reasoning about complex requirements in a uniform setting
Manuel A. Martins, Alexandre Madeira, Luís Soares Barbosa · Portuguese National Funding Agency for Science, Research and Technology (RCAAP Project by FCT) · 2011
Abstract. The paper formulates HEQ, an institution for hybrid equa-tional 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 specifica-tion of data and behavioural constraints of reconfigurable systems. 1 The problem Fundamental infrastructures of modern societies, including those related to fi-nancial, health, education, energy and water supply, are critically based on in-formation systems, which are assumed to be trustworthy. Moreover, our way of living depends on software whose reliability is crucial for our own work, se-curity, privacy, and quality of life. This explains why the quest for programs whose correctness could be established by mathematical reasoning, which has