Backward transformation of formulas in symbolic modeling: from the result to the source formula

A.B. Godlevsky, S.V. Potienko

Abstract


Logical formulas over attributes set are analog of system states in symbolic modeling of transition systems. Transition rules of source system are the base for building of modeling rules which operate on formula state and define transition from source state to the next or previous state. Predicate transformer is an algorithm which models transitions in the formula state space. We describe backward predicate transformer which has distinguishing feature that modeled transitions allow as assignment operators over simple and complex data structures (arrays and lists) as constraints which define attribute changes implicitly.

Problems in programming 2010; 2-3:363-368


References


Floyd R. W. «Assigning Meaning to Programs», in Proceedings of Symposium on Applied Mathematics, Vol. 19, J.T. Schwartz (Ed.), A.M.S.,

– Р. 19–32.

Hoare C. A. R. «An axiomatic basis for computer programming». Communications of the ACM, 12(10): 576–580, 583 October 1969.

Летичевский А.А., Капитонова Ю.В., Волков В.А., Летичевский А.А. (мл.), Баранов С.Н., Котляров В.П., Вейгарт Т. Спецификация

систем с помощью базовых протоколов // Кибернетика и системный анализ – № 4. –2005.

Потиенко С.В. Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами // Проблеми

програмування. – 2008. – № 4. – С. 39–45.


Refbacks

  • There are currently no refbacks.