Correctness of programs with Pascal-like procedures without global variables

DOI10.1016/0304-3975(84)90066-5zbMATH Open0534.68016OpenAlexW2026086747MaRDI QIDQ790607FDOQ790607

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

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

zbMATH Keywords

expressivenessHoare-like systemsecond-order theory

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (3)

• Proof obligations for blocks and procedures
• Reasoning about procedures as parameters in the language L4
• Title not available (Why is that?)

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)