This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Note on Synthesis of Inductive Assertions
January 1980 (vol. 6 no. 1)
pp. 32-39
S.K. Basu, Department of Computer Science, University of Nebraska
One of the principal impediments to widespread use of automated program verification methodology is due to the user burden of creating appropriate inductive assertions. In this paper, we investigate a class of programs for which such inductive assertions can be mechanically generated from Input-output specifications. This class of programs, called accumulating programs, are iterative realizations of problems in which the required output information is accumulated during successive passes over the input data structures. Obtaining invariant assertions for such programs is shown to be equivalent to the problem of generalizations of specifications to that over an extended closed data domain. For this purpose, a set of basis data elements are to be conceived of as generating the extended domain. An arbitary data element would thus be considered as uniquely decomposable into a sequence of basis elements. The structural relations between the components of a data element are used to extend program behavior and thus obtain the desired invariant.
Index Terms:
program verification, Accumulating programs, inductive assertions, linear data domain
Citation:
S.K. Basu, "A Note on Synthesis of Inductive Assertions," IEEE Transactions on Software Engineering, vol. 6, no. 1, pp. 32-39, Jan. 1980, doi:10.1109/TSE.1980.230460
Usage of this product signifies your acceptance of the Terms of Use.