Page 54 - 4868

Ошибка! Стиль не определен. 52

Запитання для самоперевірки

1. Які дві форми синхронізації Ви знаєте?
2. Що розуміють під дрібномодульною неподільною дією у термінах
паралельної програми?
3. Якими основними характеристиками повинні володіти обчислювальні
машини для можливості розпаралелення програми?
4. Що розуміють під критичним посиланням у термінах паралельної
програми?
5. У яких випадках у паралельній програмі задовольняється умова «не
більше одного»?
6. Що розуміють під крупномодульною неподільною дією у термінах
паралельної програми?
7. Для чого використовуються символи « < » та « > » у паралельній
програмі?
8. Які форми оператора await Ви знаєте?
9. Що таке безумовна та умовна неподільна дія?
10. У якому випадку процес знаходиться в стані активного очікування?

ЛЕКЦІЯ 8. АКСІОМАТИЧНА СЕМАНТИКА ПАРАЛЕЛЬНИХ

ПРОГРАМ

8.1. Основні визначення та поняття
Стверджуючі міркування дозволяють зрозуміти властивості паралельної
програми. Але, що ще важливіше, вони можуть допомогти в розробці
правильних програм. Основою для тверджень є так звана логіка
програмування (ЛП)– формальна логічна система, яка забезпечує породження
точних тверджень про виконання програми.
Будь-яка формальна логічна система складається з правил, визначених у
термінах наступних множин:
1) символів;
2) формул, побудованих з цих символів;
3) виділених формул, що називаються аксіомами;
4) правил виведення.
Формулами є правильно побудовані послідовності символів. Аксіоми –
це особливі формули, які апріорі передбачаються як істинні. Правила
виведення визначають, як отримати справжні формули з аксіом та інших
істинних формул. Правила виведення мають наступний вигляд:
H , H ,..., H
1 2 n
,
C
де H – гіпотеза, а C – висновок. Значення правила виведення полягає в тому,
i
що якщо всі гіпотези істинні, то і висновок істинний. І гіпотези, і висновок є
формулами або їх схематичним поданням.
Доведення у формальній логічній системі – це послідовність рядків,