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.
No takes yet. Share an insight, caveat, or question.
Michel Sintzoff (1972) studied this question.
Synapse has enriched 2 closely related papers on similar clinical questions. Consider them for comparative context: