Hoare-style reasoning from multiple contracts

Abstract

Modern software is often developed with advanced mechanisms for code reuse. A software module may build on other software modules or libraries where the source code is not available. And even if the source code is known, the binding mechanism may be such that the binding of methods is not known at verification time, and thus the underlying reused code cannot be determined. For example, in delta- oriented programming the binding of methods depends on the ordering of deltas in each product, making modular reasoning non-trivial. Similar problems occur with traits and subclassing. Reasoning inside a module must then be based on partial knowledge of the methods, typically given by contracts in the form of pairs of pre- and post-conditions, and one may not derive new properties by re-verification of the (unavailable) source code. In the setting of Hoare logic, this gives some challenges to general rules for adaptation that goes beyond traditional systems for Hoare logic. We develop a novel way of reasoning from multiple contracts, which makes the traditional adaptation rules superfluous. The problem we address does not depend on the choice of programming language. We therefore focus on general rules rather than statement-specific rules. We show soundness and completeness for the suggested rules.