Towards the Future: Bring Program Correctness back to the focus

TL;DR

This paper advocates for re-emphasizing program correctness by leveraging semantic theories and developing automated tools based on OESPA to ensure future software reliability.

Contribution

It introduces the concept of conditional semantic predicates and redefines semantic calculus to facilitate automatic correctness proofs for large programs using OESPA.

Findings

Semantic functions and predicates are re-represented for automation.

A new semantic calculus illustrates how to compute semantics automatically.

Foundation laid for developing tools to verify program correctness at scale.

Abstract

Program correctness used to be the main concern of computer software in the early days when formal semantics was a hot topic. But, the word "correct" was afterwards replaced by reliable, robust and trustworthy etc., a tradeoff situation then. This is not because correctness is no longer important, but because people found no way to get through in this direction. The tradeoff has led software engineers to focus on techniques and testing tools. Rapid development of software engineering has now reached a peak and programmers are now working freely without worrying too much about bugs, since bugs are not avoidable anyway. Is it meaningful to talk about program correctness today? Our answer is yes. It is the time to seriously consider correctness again, before it is too late, to prepare for the future. Future generation computer systems should be correct, both syntactically (statically) and semantically (dynamically). The book "OESPA: Semantic Oriented Theory of Programming" (2019) by the first author has opened a new direction for semantic study. Theoretically speaking, it is possible now, based on OESPA, to compute program semantics from program text so that program correctness could be proved. But, semantic computations and correctness proving cannot be done by hand when the size of a program is big. Automatic tools are necessary. This paper tries to lay a foundation for developing needed auto tools, so that OESPA is enriched to serve future need. To this end, a new concept named conditional semantic predicate is proposed. Concepts in OESPA, including semantic functions, semantic predicates, semantic formulas and semantic calculus, are re-represented in accordance. Such re-introduction is necessary since the book is the only publication on semantic calculus so far. The new version of semantic calculus illustrates how semantics auto-computation would be carried out.