A Hoare Logic Contract Theory : An Exercise in Denotational Semantics

• We sketch a simple theory of Hoare logic contracts for programs with procedures, presented in denotational semantics. In particular, we give a simple semantic justification of the usual procedure-modular treatment of such programs. The justification is given by means of a proof of soundness of a contract-relative denotational semantics against the standard denotational semantics of procedures in the context of procedure declarations. The suggested formal development can be used as an inspiration for more ambitious contract theories.

Subject headings

HUMANIORA  -- Filosofi, etik och religion -- Filosofi (hsv//swe)

HUMANITIES  -- Philosophy, Ethics and Religion -- Philosophy (hsv//eng)

NATURVETENSKAP  -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences -- Computer Sciences (hsv//eng)

Publication and Content Type

vet (subject category)

kap (subject category)