Article

Free access

Calculating properties of programs by valuations on specific models

Author:

Michel SintzoffAuthors Info & Claims

Proceedings of ACM conference on Proving assertions about programs

Pages 203 - 207

https://doi.org/10.1145/800235.807086

Published: 01 January 1972 Publication History

PDF eReader

Abstract

The proof that a program verifies some property is carried out by the valuation of the program in a model characterizing that property. Specific models are given for sufficient conditions of the correctness of types, locations and asynchronous computations; a hypothetical programming language is used, which includes functions and locations and allows their recursive composition. The application of the method in studying termination or correctness problems is discussed on particular programs.

References

[1]

Naur P., Checking of operand types in ALGOL compilers, BIT 5 (1965), 151-163.

Crossref

Google Scholar

[2]

Van Wijngaarden A. (ed.), B. J. Mailloux, J.E.L. Peck and C.H.A. Koster, Report on the algorithmic language ALGOL68, Num. Math. 14 (1969), 79-218.

Digital Library

Google Scholar

[3]

Cooper D. C., Programs for mechanical program verification, in "Machine Intelligence 6", pp. 43-59, Edinburgh Univ. Press, 1971.

Google Scholar

[4]

Curry H. B., R. Feys, Combinatory logic, North-Holl., Amsterdam, 1958.

Google Scholar

[5]

King J. C., A program verifier, Ph.D. Thesis, Carnegie-Mellon Univ., 1969.

Digital Library

Google Scholar

[6]

Manna Z., Mc Carthy J., Properties of programs and partial function logic, in "Machine Intelligence5", pp. 27-38, Edin. Univ. Press, 1969.

Google Scholar

[7]

Burstall R. M., Proving properties of programs by structural induction, Comp. J. 12(1969), 41-49.

Crossref

Google Scholar

[8]

Reynolds J.C., GEDANKEN-A simple typeless language based on the principle of completeness and the reference concept, Comm. ACM 13(1970), 308-319.

Digital Library

Google Scholar

Cited By

View all

Kryvyi SMaksymets O(2013)Program VerificationCybernetics and Systems Analysis10.1007/s10559-013-9569-149:6(805-814)Online publication date: 1-Nov-2013
https://dl.acm.org/doi/10.1007/s10559-013-9569-1
Jones N(2005)Flow analysis of lambda expressionsAutomata, Languages and Programming10.1007/3-540-10843-2_10(114-128)Online publication date: 25-May-2005
https://doi.org/10.1007/3-540-10843-2_10
Dershowitz N(2004)Termination by AbstractionLogic Programming10.1007/978-3-540-27775-0_1(1-18)Online publication date: 2004
https://doi.org/10.1007/978-3-540-27775-0_1
Show More Cited By

Index Terms

Calculating properties of programs by valuations on specific models
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Correctness
2. Theory of computation
  1. Logic
    1. Proof theory

Recommendations

Calculating properties of programs by valuations on specific models
Proceedings of ACM conference on Proving assertions about programs

The proof that a program verifies some property is carried out by the valuation of the program in a model characterizing that property. Specific models are given for sufficient conditions of the correctness of types, locations and asynchronous ...
Calculating properties of programs by valuations on specific models
Proceedings of ACM conference on Proving assertions about programs

The proof that a program verifies some property is carried out by the valuation of the program in a model characterizing that property. Specific models are given for sufficient conditions of the correctness of types, locations and asynchronous ...
Verifying properties of parallel programs: an axiomatic approach

An axiomatic method for proving a number of properties of parallel programs is presented. Hoare has given a set of axioms for partial correctness, but they are not strong enough in most cases. This paper defines a more powerful deductive system which is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Proceedings of ACM conference on Proving assertions about programs

January 1972

215 pages

ISBN:9781450378918

DOI:10.1145/800235

ACM SIGPLAN Notices Volume 7, Issue 1
Proceedings of ACM conference on Proving assertions about programs
January 1972
211 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/942578
Issue’s Table of Contents
ACM SIGACT News Just Accepted
Proceedings of ACM conference on Proving assertions about programs
January 1972
211 pages
ISSN:0163-5700
DOI:10.1145/942580
Issue’s Table of Contents

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1972

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

42
Total Citations
View Citations
427
Total Downloads

Downloads (Last 12 months)104
Downloads (Last 6 weeks)25

Reflects downloads up to 30 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Kryvyi SMaksymets O(2013)Program VerificationCybernetics and Systems Analysis10.1007/s10559-013-9569-149:6(805-814)Online publication date: 1-Nov-2013
https://dl.acm.org/doi/10.1007/s10559-013-9569-1
Jones N(2005)Flow analysis of lambda expressionsAutomata, Languages and Programming10.1007/3-540-10843-2_10(114-128)Online publication date: 25-May-2005
https://doi.org/10.1007/3-540-10843-2_10
Dershowitz N(2004)Termination by AbstractionLogic Programming10.1007/978-3-540-27775-0_1(1-18)Online publication date: 2004
https://doi.org/10.1007/978-3-540-27775-0_1
Jensen T(1997)Disjunctive program analysis for algebraic data typesACM Transactions on Programming Languages and Systems10.1145/265943.26596619:5(751-803)Online publication date: 1-Sep-1997
https://dl.acm.org/doi/10.1145/265943.265966
Cousot PCousot R(1992)Abstract interpretation and application to logic programsJournal of Logic Programming10.1016/0743-1066(92)90030-713:2-3(103-179)Online publication date: 1-Jul-1992
https://dl.acm.org/doi/10.1016/0743-1066%2892%2990030-7
Jones NMycroft A(1986)Data flow analysis of applicative programs using minimal function graphsProceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages10.1145/512644.512672(296-306)Online publication date: 1-Jan-1986
https://dl.acm.org/doi/10.1145/512644.512672
Jones NMuchnick SDeMillo R(1982)A flexible approach to interprocedural data flow analysis and programs with recursive data structuresProceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/582153.582161(66-74)Online publication date: 25-Jan-1982
https://dl.acm.org/doi/10.1145/582153.582161
Holley LRosen B(1981)Qualified Data Flow ProblemsIEEE Transactions on Software Engineering10.1109/TSE.1981.2345097:1(60-78)Online publication date: 1-Jan-1981
https://dl.acm.org/doi/10.1109/TSE.1981.234509
Holley LRosen BAbrahams PLipton RBourne S(1980)Qualified data flow problemsProceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/567446.567454(68-82)Online publication date: 28-Jan-1980
https://dl.acm.org/doi/10.1145/567446.567454
Jones NMuchnick S(1980)Complexity of flow analysis, inductive assertion synthesis and a language due to DijkstraProceedings of the 21st Annual Symposium on Foundations of Computer Science10.1109/SFCS.1980.16(185-190)Online publication date: 13-Oct-1980
https://dl.acm.org/doi/10.1109/SFCS.1980.16
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Calculating properties of programs by valuations on specific models

Calculating properties of programs by valuations on specific models

Verifying properties of parallel programs: an axiomatic approach