Author(s)
Anureev Igor
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
Computer Science, № 15, 2001
Pages
1-16