Procedure Call Proof Rules and Their Applications
Summary :
This paper presents consize proof rules for procedure calls in Pascal-like programs. Procedures which we deal with may contain recursive calls and have both variable parameters and value parameters. For simplicity, we place two restrictions on procedures. (1) Non-local variables are not allowed to appear in any procedures. (2) All parameters of procedures are of integer type. We have attempted to make the proof rules clear, understandable, and easy to apply to program verification. Our proof rules are readily used to aid in generating verification conditions in mechanical verifiers. We present several examples so as to show how these proof rules can be used to facilitate varification of programs with procedure calls.
- Publication
- IEICE TRANSACTIONS on transactions Vol.E65-E No.6 pp.318-324
- Publication Date
- 1982/06/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- PAPER
- Category
- Automata and Languages
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Keijiro ARAKI, Kazuo USHIJIMA, "Procedure Call Proof Rules and Their Applications" in IEICE TRANSACTIONS on transactions,
vol. E65-E, no. 6, pp. 318-324, June 1982, doi: .
Abstract: This paper presents consize proof rules for procedure calls in Pascal-like programs. Procedures which we deal with may contain recursive calls and have both variable parameters and value parameters. For simplicity, we place two restrictions on procedures. (1) Non-local variables are not allowed to appear in any procedures. (2) All parameters of procedures are of integer type. We have attempted to make the proof rules clear, understandable, and easy to apply to program verification. Our proof rules are readily used to aid in generating verification conditions in mechanical verifiers. We present several examples so as to show how these proof rules can be used to facilitate varification of programs with procedure calls.
URL: https://global.ieice.org/en_transactions/transactions/10.1587/e65-e_6_318/_p
Copy
@ARTICLE{e65-e_6_318,
author={Keijiro ARAKI, Kazuo USHIJIMA, },
journal={IEICE TRANSACTIONS on transactions},
title={Procedure Call Proof Rules and Their Applications},
year={1982},
volume={E65-E},
number={6},
pages={318-324},
abstract={This paper presents consize proof rules for procedure calls in Pascal-like programs. Procedures which we deal with may contain recursive calls and have both variable parameters and value parameters. For simplicity, we place two restrictions on procedures. (1) Non-local variables are not allowed to appear in any procedures. (2) All parameters of procedures are of integer type. We have attempted to make the proof rules clear, understandable, and easy to apply to program verification. Our proof rules are readily used to aid in generating verification conditions in mechanical verifiers. We present several examples so as to show how these proof rules can be used to facilitate varification of programs with procedure calls.},
keywords={},
doi={},
ISSN={},
month={June},}
Copy
TY - JOUR
TI - Procedure Call Proof Rules and Their Applications
T2 - IEICE TRANSACTIONS on transactions
SP - 318
EP - 324
AU - Keijiro ARAKI
AU - Kazuo USHIJIMA
PY - 1982
DO -
JO - IEICE TRANSACTIONS on transactions
SN -
VL - E65-E
IS - 6
JA - IEICE TRANSACTIONS on transactions
Y1 - June 1982
AB - This paper presents consize proof rules for procedure calls in Pascal-like programs. Procedures which we deal with may contain recursive calls and have both variable parameters and value parameters. For simplicity, we place two restrictions on procedures. (1) Non-local variables are not allowed to appear in any procedures. (2) All parameters of procedures are of integer type. We have attempted to make the proof rules clear, understandable, and easy to apply to program verification. Our proof rules are readily used to aid in generating verification conditions in mechanical verifiers. We present several examples so as to show how these proof rules can be used to facilitate varification of programs with procedure calls.
ER -
English
