Abstract

A new specification language, simple to master, is suggested. In spite of simplicity, this language is expressive enough. A decision method for its quantifier-free formulas is given. A program verification method based on this language is illustrated by an example of a program of bubble sorting.

File
anureev.pdf124.77 KB
Issue
Pages
1-16