Метод доведення властивостей програм в композиційно-номінативних мовах IPCL

• Дата: 2008
• Автор: Панченко, Т.В.
• Формат: Стаття
• Мова: Ukrainian
• Опубліковано: Інститут програмних систем НАН України 2008
• Теми: Теоретичні та методологічні основи програмування
• Онлайн доступ: https://nasplib.isofts.kiev.ua/handle/123456789/329
• Назва журналу: Digital Library of Periodicals of National Academy of Sciences of Ukraine
• Цитувати: Метод доведення властивостей програм в композиційно-номінативних мовах IPCL / Т.В. Панченко // Пробл. програмув. — 2008. — N 1. — С. 3-16. — Бібліогр.: 33 назв. — укр.

Викладено композиційний метод верифікації систем спеціального класу – моделі багатоекземплярного виконання програм у серверному середовищі з паралелізмом у режимі почергового виконання з пере ключенням і взаємодією через спільну пам’ять. У роботі специфіковано задачу, побудовано відповідні моделі, сформульовано два варіанти часткової коректності програм на введених композиційних мовах та запропоновано методологію верифікації, що включає метод з лінійною складністю замість експоненційної. The compositional method for verification of special class systems, namely multi-instance program execution model in server environment with shared memory interleaving concurrency, is presented. The task is specified and appropriate models are developed here. Two types of partial correctness properties of programs in introduced compositional languages are formulated. Methodology of verification including method with linear complexity instead of exponential one is developed here.