kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A Hoare Logic Contract Theory: An Exercise in Denotational Semantics
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Mechatronics. Systems Development Division, Scania AB, Södertälje, Sweden.ORCID iD: 0000-0002-9655-7326
Number of Authors: 22018 (English)In: Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday, Springer Nature , 2018, p. 119-127Chapter in book (Other academic)
Abstract [en]

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.

Place, publisher, year, edition, pages
Springer Nature , 2018. p. 119-127
National Category
Philosophy Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-332046DOI: 10.1007/978-3-319-98047-8_8Scopus ID: 2-s2.0-85142738285OAI: oai:DiVA.org:kth-332046DiVA, id: diva2:1783203
Note

Part of ISBN 9783319980478, ISBN 9783319980461

QC 20230719

Available from: 2023-07-19 Created: 2023-07-19 Last updated: 2023-08-04Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Gurov, DilianWestman, Jonas

Search in DiVA

By author/editor
Gurov, DilianWestman, Jonas
By organisation
Theoretical Computer Science, TCSMechatronics
PhilosophyComputer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 39 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf