A correctness proof of sorting by means of formal procedures

M.M. Fokkinga

doi:10.1016/0167-6423(87)90009-8

A correctness proof of sorting by means of formal procedures

M.M. Fokkinga

Research output: Contribution to journal › Article › Academic › peer-review

83 Downloads (Pure)

Abstract

We consider a recursive sorting algorithm in which, in each invocation, a new variable and a new procedure (using the variable globally) are defined and the procedure is passed to recursive calls. This algorithm is proved correct with Hoare-style pre- and postassertions. We also discuss the same algorithm expressed as a functional program.

Original language	Undefined
Article number	10.1016/0167-6423(87)90009-8
Pages (from-to)	263-269
Number of pages	7
Journal	Science of computer programming
Volume	9
Issue number	3
DOIs	https://doi.org/10.1016/0167-6423(87)90009-8
Publication status	Published - Dec 1987

Keywords

IR-66237
EWI-6293

Access to Document

10.1016/0167-6423(87)90009-8

Cite this

@article{ea0b04e5f6cf422ca28adcbcccde4438,

title = "A correctness proof of sorting by means of formal procedures",

abstract = "We consider a recursive sorting algorithm in which, in each invocation, a new variable and a new procedure (using the variable globally) are defined and the procedure is passed to recursive calls. This algorithm is proved correct with Hoare-style pre- and postassertions. We also discuss the same algorithm expressed as a functional program.",

keywords = "IR-66237, EWI-6293",

author = "M.M. Fokkinga",

note = "Imported from EWI/DB PMS [db-utwente:arti:0000003417]",

year = "1987",

month = dec,

doi = "10.1016/0167-6423(87)90009-8",

language = "Undefined",

volume = "9",

pages = "263--269",

journal = "Science of computer programming",

issn = "0167-6423",

publisher = "Elsevier",

number = "3",

}

TY - JOUR

T1 - A correctness proof of sorting by means of formal procedures

AU - Fokkinga, M.M.

N1 - Imported from EWI/DB PMS [db-utwente:arti:0000003417]

PY - 1987/12

Y1 - 1987/12

N2 - We consider a recursive sorting algorithm in which, in each invocation, a new variable and a new procedure (using the variable globally) are defined and the procedure is passed to recursive calls. This algorithm is proved correct with Hoare-style pre- and postassertions. We also discuss the same algorithm expressed as a functional program.

AB - We consider a recursive sorting algorithm in which, in each invocation, a new variable and a new procedure (using the variable globally) are defined and the procedure is passed to recursive calls. This algorithm is proved correct with Hoare-style pre- and postassertions. We also discuss the same algorithm expressed as a functional program.

KW - IR-66237

KW - EWI-6293

U2 - 10.1016/0167-6423(87)90009-8

DO - 10.1016/0167-6423(87)90009-8

M3 - Article

VL - 9

SP - 263

EP - 269

JO - Science of computer programming

JF - Science of computer programming

SN - 0167-6423

IS - 3

M1 - 10.1016/0167-6423(87)90009-8

ER -