scientific article; zbMATH DE number 3888897

MaRDI QIDQ3221385zbMATH OpenFDO

Authors Nikolaĭ Nikolaevich Kosovskiĭ

Publication date 1983

zbMATH Keywords

localized variables callpartial correctnessrecursive procedure

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Proof rules for recursive procedures
• A general proof rule for procedures in predicate transformer semantics
• scientific article; zbMATH DE number 4005583
• A Structure-directed Total Correctness Proof Rule for Recursive Procedure Calls
• A partial correctness proof for programs with decided specification

Cited in

(9)

• A correctness proof of sorting by means of formal procedures
• A sharp proof rule for procedures in WP semantics
• Proof rules for recursive procedures
• Unifying Recursion in Partial, Total and General Correctness
• A Structure-directed Total Correctness Proof Rule for Recursive Procedure Calls
• scientific article; zbMATH DE number 4005583 (Why is no real title available?)
• A partial correctness proof for programs with decided specification
• Correctness of programs with Pascal-like procedures without global variables
• Inference rules for proving the equivalence of recursive procedures

This page was built for publication:

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