Подано приклад детального доведення коректності класичної задачі паралельного додавання до спільної комірки пам"яті за допомогою методу доведення властивостей програм в композиційних мовах IPCL. Надано опис методу та його порівняння з іншими.
Ключові слова: композиційне програмування, верифікація програм, модель виконання програм, часткова коректність, паралельне програмування, інваріант, транзиційні системи, спільна змінна, спільна пам"ять.
The example of detailed correctness proof for classical task of parallel addition to shared variable using the method for program properties proof in compositional languages IPCL is given here. The method is described and compared to others in this paper.
Key Words: compositional programming, program verification, program execution model, partial correctness, safety, parallel programming, shared memory concurrency, invariant, transition system, shared variable, shared memory.
