A correctness proof of sorting by means of formal procedures

M.M. Fokkinga

    Research output: Contribution to journalArticleAcademicpeer-review

    97 Downloads (Pure)


    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 languageUndefined
    Article number10.1016/0167-6423(87)90009-8
    Pages (from-to)263-269
    Number of pages7
    JournalScience of computer programming
    Issue number3
    Publication statusPublished - Dec 1987


    • IR-66237
    • EWI-6293

    Cite this