Predicate transformers in the context of symbolic modeling of transition systems |
| |
Authors: | A B Godlevsky |
| |
Affiliation: | 1.Cybernetics Institute,National Academy of Sciences of Ukraine,Kiev,Ukraine |
| |
Abstract: | In modelling attribute transition systems, classes of their states can be described in a given signature of functional and
predicate symbols. A procedure is developed for transforming such formulas by assignment operators and the obtained formulas
are proved to correspond to strongest postconditions. A peculiarity of this paper is that functional-type attributes can be
used in specifying transition systems, in particular, their array-type attributes. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|