A formal model for verification of abstract properties
Victor Winter, Brian T. Smith, G.H. Chisholm, Anthony S. Wojcik · 1992
We are given a specification s that states the requirements of a problem in terms of data dependencies. We are also given some assumptions about the input domain. In this paper we define a formal model that can be used to verify that a program written according to the specification s does indeed have the data dependencies specified by s.