Predicate transformers in the context of symbolic modeling of transition systems

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.