Correctness of programs with Pascal-like procedures without global variables

DOI10.1016/0304-3975(84)90066-5MaRDI QIDQ790607zbMATH OpenOpenAlexFDO

Authors Ernst-Rüdiger Olderog

Publication date 1984

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(84)90066-5

zbMATH Keywords

expressivenessHoare-like systemsecond-order theory

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Correctness of on-line partial evaluation for a Pascal-like language
• scientific article; zbMATH DE number 3936484
• scientific article; zbMATH DE number 3888897
• Publication:4934533
• An elementary and unified approach to program correctness
• Correctness of programs which calculate recurrent consequences
• Implementation of Functional Languages
• Correctness of procedure representations in higher-order assembly language

Cites work

• scientific article; zbMATH DE number 3835316 (Why is no real title available?)
• scientific article; zbMATH DE number 3655320 (Why is no real title available?)
• scientific article; zbMATH DE number 3688676 (Why is no real title available?)
• scientific article; zbMATH DE number 3705887 (Why is no real title available?)
• scientific article; zbMATH DE number 3707731 (Why is no real title available?)
• scientific article; zbMATH DE number 3731315 (Why is no real title available?)
• scientific article; zbMATH DE number 3755838 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3351184 (Why is no real title available?)
• A sound and relatively* complete Hoare-logic for a language with higher type procedures
• An axiomatic basis for computer programming
• Effective Axiomatizations of Hoare Logics
• First-order dynamic logic
• Generic commands--a tool for partial correctness formalisms
• On correct procedure parameter transmission in higher programming languages
• On termination problems for finitely interpreted ALGOL-like programs
• On the notion of expressiveness and the rule of adaptation
• Pascal. User manual and report. 2nd ed
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• Sound and complete Hoare-like calculi based on copy rules
• Soundness and Completeness of an Axiom System for Program Verification
• Ten Years of Hoare's Logic: A Survey—Part I
• The IO- and OI-hierarchies
• The formal termination problem for programs with finite ALGOL 68-modes

Cited in

(3)

• Proof obligations for blocks and procedures
• Reasoning about procedures as parameters in the language L4
• scientific article; zbMATH DE number 3858385 (Why is no real title available?)

Describes a project that uses

Uses Software

• ALGOL 68

This page was built for publication: Correctness of programs with Pascal-like procedures without global variables

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q790607)