A WP-calculus for OO

The work

AuthorsFrank S. de Boer
Editors
Typeinproceedings
Year1999
Citekeyboer1999wpcalculus

Where it appeared

Published inFoundations of Software Science and Computation Structures
PublisherSpringer
SeriesLecture Notes in Computer Science
Number in series1578
Pages135--149

Abstract

A sound and complete Hoare-style proof system is presented for a sequential object-oriented language, called SPOOL. The proof system is based on a weakest precondition calculus for aliasing and object-creation.

A copy is held

pdf, 405.1 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via openalex
Added2026-08-04 00:00 UTC
Approved bya person 2026-08-18 16:22 UTC

Cite it as

@inproceedings{boer1999wpcalculus,
  title        = {A WP-calculus for OO},
  author       = {Frank S. de Boer},
  year         = {1999},
  booktitle    = {Foundations of Software Science and Computation Structures},
  publisher    = {Springer},
  series       = {Lecture Notes in Computer Science},
  pages        = {135--149},
  doi          = {10.1007/3-540-49019-1_10},
}

This record lives at https://refs.drheap.org/boer1999wpcalculus/ and will keep doing so.