Calculating with procedure calls
type: Item
instance of: scholarly article
title: Calculating with procedure calls
zbMATH Open document ID: 0791.68105
DOI: 10.1016/0020-0190(93)90098-T
author: A. Bijlsma
published in: Information Processing Letters
publication date: 1993-10-17T00:00:00Z
review text: Various proof rules for procedure calls in weakest precondition semantics have been proposed. The author gives a proof rule that is very easy to use, but does not yield the best possible answer for every specification -- only for a large class of specifications called normal specifications. In the Appendix, he shows how every specification can be transformed into an equivalent normal one.
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 417421
zbMATH Keywords: formal semantics
zbMATH Keywords: program specification
zbMATH Keywords: program correctness
zbMATH Keywords: procedures
zbMATH Keywords: proof rules
reviewed by: Satoshi Miura
MaRDI profile type: Publication
cites work: A sharp proof rule for procedures in WP semantics
cites work: Q4692630
cites work: Q3925859
cites work: A general proof rule for procedures in predicate transformer semantics
full work available at URL: 0020-0190(93)90098-t
OpenAlex ID: W2129304035
description: scientific article; zbMATH DE number 417421