2001年京都賞受賞講演 Assertions: a personal perspective〔英文〕
スポンサーリンク
概要
- 論文の詳細を見る
An assertioin is a Boolean formula writtern in the text of a program, at a place where its evaluation will always be ture-or at least, that is the intention of the programmer. In the absence of jumps, it specifies the internal interface between the part of the program tahat comes begore it and the part that comes after. The interface between a procedure delaration and its call is defined by assertions known as preconditions and post-condition. If the assertions are strong enough, they express everything that the programmers on eitheer side of the interface need to kyow about the program on the other side, even before the code is written. Indeed, such strong assertions can serve as the basis ot a formal proof ot hte correctness of a complete program. In this paper, I will describe how my early experience in industry triggered my interest in assertions and thier role in program proof; and how my subsequent research at university extended the idea into a methodology for the specification and design of programs. Now that I have returned to work in industry, I have had the opportunity to investigate the current role of assertions in industrial program development. My personal perspective illustrates the complementary roles of pure research, aimed at academic ideals of excellence, and the unexpected ways in which the results of such research contribute to the gradual improvement of engineering practice.
- 一般社団法人日本ソフトウェア科学会の論文
- 2001-07-16