Модель програмування - це математична модель, яка надає семантичне значення завдань і програм, визначає будівельні операції над задачами та програмами та вказує, коли програма вирішує завдання. Ми говоримо про реляційну модель, якщо елементи семантичних доменів є реляційними.

Давайте подумаємо над завданням програмування [[. Ми виходимо з концепції майбутнього 83]]. Завдання програмування завжди виконується за ключем стану [[. Премія 76]]. Щоб сформулювати проблему, ми повинні створити математичну модель задачі, яка використовується в загальному розумінні. Якщо ми думаємо про концепцію моделі, яка використовується в математичній логіці, теорії моделей, ми посилаємося на неї окремо. Формулювання завдання не може бути прив’язане до напр. до фіксованої часової логічної структури, оскільки в цьому випадку завдання вже не може бути сформульовано незалежно від програми, що визначає структуру часу. Ми не ототожнюємо проблему з набором формул, що її описують, а також з синтаксичними одиницями, оскільки неінтерпретований набір формул має як семантичне значення у всіх інтерпретаціях. Завдання завжди задається у фіксованому просторі станів за допомогою мається на увазі відношень., Потрібна абстракція. Шлях, що веде до формулювання завдання, зараз не вивчається. Ми не досліджуємо, чи справді формальна форма завдання описує завдання, сформульоване якоюсь природною мовою. Розглядаючи це питання в рамках обраної моделі програмування.

19.1. Завдання: годування філософів

Наш перший приклад - від Е. В. Дейкстрема, який проілюстрував принцип розподілу ресурсів на основі виключення між процесами в процесі навчання операційним системам. Цей приклад моделює систему, яка працює з паралельного процесу, що працює разом. Згідно з історією, за столом є п’ятеро філософів, які можуть купити макарони з великого загального столу. Щоб макарони потрапили в кімнату, потрібні дві виделки. Їжу можна вживати кілька разів за раз, але кожну з вилок, необхідних для їжі, потрібно виконувати окремо, щоб одночасно їх вживав лише один філософ. Для кожного філософа є дві вілли, але це вілли, якими хочуть скористатися ваші сусіди. Якщо філософ піднімає ліву і праву виделки зі столу і їсть, ніхто з сусідів не може мати двох виделок, необхідних для їжі. Одночасно їсти можуть лише сусідні філософи .

19.1. ббра. Філософи їдальні

годування філософів

Позначте це. з філософією, а кожна форма з ініціалами: thinking:, тримаючи виделку в руці:, eat:, бути вдома:. Далі наводяться приклади формулювання вимог до специфікації поведінки філософів.