Специфікація мови програмування

Специфікація мови програмування (або стандарт чи визначення) є документацією, яка визначає мову програмування, так, щоб користувачі та розробники мови програмування могли дійти згоди, що означають програми на цій мові. Специфікації, як правило, деталізовані та формальні, і в першу чергу використовуються розробниками, при цьому користувачі посилаються на них у разі неоднозначності; специфікації мови C++ часто критикуються користувачами, наприклад, через складність. Відповідна документація включає в себе керівництво по мові програмування, яке призначено виключно для користувачів, і обґрунтування мови програмування та пояснює, чому специфікація написана так як є; вони, як правило, більш неформальні, ніж специфікація.

Стандартування

Не всі основні мови програмування мають специфікації, і мови можуть існувати і бути популярними протягом десятиліть без специфікації. Мова може мати одну або більше реалізацій, чия поведінка діє де-факто як стандарт, без того, щоб ця поведінка документувалася в специфікації. Perl (після Perl 5) є відомим прикладом мови без специфікації, тоді як PHP отримав специфікацію лише в 2014 році, після 20 років використання. Мова може бути спочатку реалізована, а потім отримати специфікацію, або спочатку отримати специфікацію, і вже потім реалізована, або ці два процеси можуть відбуватись одночасно, що є поширеною практикою. Це пояснюється тим, що реалізації та специфікації забезпечують перевірку один одного: написання специфікації вимагає точного зазначення поведінки реалізації, а реалізація перевіряє, що специфікація можлива, практична та послідовна. Написання специфікації перед реалізацією здебільшого не відбувалось з часів ALGOL 68 (1968) через несподівані труднощі в реалізації, коли реалізація потім відкладалась. Проте, мови все ще іноді реалізуються і набувають популярності без формальної специфікації: реалізація є необхідною для використання, тоді як специфікація є бажаною, але не істотною.

	Алгол 68 був першою (і, можливо, однією з останніх) мовою, яка була повністю формально визначена, перш ніж вона була реалізована
— Корнеліс Костер,

Форми

Специфікація мови програмування може мати декілька форм, включаючи наступні:

• Явне визначення синтаксису і семантики мови. Хоча синтаксис зазвичай визначається з використанням формальної граматики, семантичні визначення можуть бути написані природною мовою (наприклад, підхід, прийнятий для мови С), або формальної семантики (наприклад, Standard ML та Scheme специфікації). Відомим прикладом є мова С, яка набула популярності без формальної специфікації, натомість, вона була описана у книзі Мова програмування C (1978), і лише набагато пізніше формально стандартизована в ANSI C (1989).
• Опис поведінки компілятора (іноді званий «транслятор») для мови (наприклад, мова C++ і Fortran). Синтаксис і семантика мови повинні виводитись з цього опису, який може бути написаний природною або формальною мовою.
• Еталонна реалізація, іноді написана мовою, що задається (наприклад, Prolog). Синтаксис і семантика мови виражені у поведінці еталонної реалізації.

Синтаксис

Синтаксис мови програмування зазвичай описується за допомогою комбінації наступних двох компонентів:

• регулярний вираз, що описує його лексема
• контекстно-вільна граматика, яка описує, як лексеми можуть бути об'єднані, щоб сформувати синтаксично правильну програму.

Семантика

Формулювання суворої семантики великої, складної, практичної мови програмування є складним завданням навіть для досвідчених фахівців, і кінцева специфікація може бути важкою для розуміння для будь-кого, окрім експертів. Нижче наведено деякі способи опису семантики мови програмування; всі мови використовують принаймні один з цих методів опису, а деякі мови поєднують декілька

• Природна мова: Опис природною мовою людини.
• Формальна семантика: Математичний опис.
• Еталонна реалізація: Опис за допомогою комп'ютерної програми.
• Набір тестів: Опис за допомогою прикладів програм та їх очікуваної поведінки. Хоча деякі специфікації мов створюються за допомогою наборів тестів, на еволюцію деяких специфікацій мови вплинула семантика набору тестів (наприклад, у минулому специфікація Ada була змінена, у відповідності до поведінки комплекту тестів для оцінки відповідності Ада (ACATS)).

Природна мова

Найбільш широко використовувані мови задаються з використанням природних мовних описів їх семантики. Цей опис зазвичай має форму довідника мови. Ці посібники можуть мати сотні сторінок, наприклад, паперова версія довідника «Специфікація мови Java, 3-е видання» містить 596 сторінок.

Неточність природної мови як засобу для опису семантики мови програмування може призвести до проблем з інтерпретацією специфікації. Наприклад, семантики потоків у Java були описані англійською мовою, згодом було виявлено, що специфікація не надає адекватного керівництва по їх реалізації для користувачів.

Формальна семантика

Формальна семантика обґрунтована математичним апаратом. Як наслідок, вони можуть бути більш точними і менш неоднозначними, ніж семантики, описані природною мовою. Однак додаткові описи семантики зроблені природною мовою часто додаються для полегшення розуміння формальних визначень. Наприклад, стандарт ISO для Modula-2 містить як формальне, так і визначення природною мовою на сусідніх сторінках.

Мови програмування, чия семантика описується формально, можуть скористатися багатьма перевагами. Наприклад:

• Формальна семантика дає можливість математичних доказів коректності програми;
• Формальна семантика полегшує розробку системи типізації, і докази доцільності цих систем типізації;
• Формальна семантика може встановлювати однозначні і єдині стандарти для реалізації мови.

Автоматична підтримка інструментів може допомогти реалізувати деякі з цих переваг. Наприклад, автоматизоване доведення теорем або перевірка теорем може збільшити впевненість програміста (або розробника мови) у правильності доведень щодо програми (або самої мови). Потужність і масштабованість цих інструментів значно варіюються: повна формальна верифікація є затратною по обчисленням, зазвичай, не масштабується для програм, розмір яких перевищує декілька сотень рядків, і може вимагати участі програміста; більш легкі інструменти, такі як перевірка моделі вимагають менших ресурсів і використовуються для програм, що містять десятки тисяч рядків; багато компіляторів застосовують статичні системи типізації до будь-якої програми, яку вони компілюють.

Еталонна реалізація

Еталонна реалізація є єдиною реалізацією мови програмування, яка позначається як авторитетна. Поведінка цієї реалізації проводиться для визначення належної поведінки програми написаній на цій мові. Цей підхід має кілька привабливих особливостей. По-перше, вона точна, і тому не вимагає людської інтерпретації: суперечки щодо сенсу програми можуть бути вирішені просто шляхом виконання програми на еталонної реалізації (за умови, що реалізація веде себе детерміновано для цієї програми).

З іншого боку, визначення семантики мови за допомогою еталонної реалізації також має ряд потенційних недоліків. Головне з них полягає в тому, що воно обмежує обмеження еталонної реалізації з властивостями мови. Наприклад, якщо в еталонній реалізації є помилка, то цю помилку слід вважати авторитетною поведінкою. Іншим недоліком є те, що програми, написані на цій мові, можуть покладатися на примхи в еталонної реалізації, перешкоджаючи портативності в різних реалізаціях.

Тим не менш, кілька мов успішно застосували підхід до базової реалізації. Наприклад, інтерпретатор Perl вважається таким, що визначає авторитетну поведінку програм Perl. У випадку з Perl, модель з відкритим вихідним кодом поширення програмного забезпечення сприяла тому, що ніхто ніколи не створював іншу реалізацію мови, тому питання, пов'язані з використанням еталонної реалізації для визначення семантики мови, є спірними.

Набір тестів

Визначення семантики мови програмування з точки зору тестового набору передбачає написання декількох прикладних програм мовою, а потім опис того, як ці програми повинні поводитися — можливо, записуючи їх правильні виходові значення. Програми, а також їхні виходові значення, називаються «набором тестів» мови. Будь-яка правильна реалізація мови повинна виробляти точні виходові дані на тестових програмах.

Головною перевагою такого підходу до семантичного опису є те, що легко визначити, чи передає мова реалізація набору тестів. Користувач може просто виконати всі програми в тестовому наборі і порівняти виходи з бажаними виходами. Проте під час використання самого підходу тестовий набір має і великі недоліки. Наприклад, користувачі хочуть запускати власні програми, які не є частиною тестового набору. Дійсно, реалізація мови, яка могла б «тільки» запускати програми у своєму тестовому наборі, була б в основному марною. Але набір тестів сам по собі не описує, як реалізація мови повинна поводитися з будь-якою програмою, яка не знаходиться в тестовому наборі; визначення того, що поведінка вимагає екстраполяції з боку виконавця, різні виконавці можуть не погодитися. Крім того, важко використовувати набір тестів для тестування поведінки, яке призначено або дозволено бути недетермінованим програмуванням.

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

Посилання

Специфікації мов програмування

Приклади специфікацій мов програмування:

• Специфікації написані здебільшого формально (математично):
  • The Definition of Standard ML, revised edition [Архівовано 16 лютого 2019 у Wayback Machine.] — формальне визначення в стилі операційної семантики.
  • Scheme R5RS [Архівовано 18 лютого 2005 у Wayback Machine.] — формальне визначення в стилі денотаційної семантики
• Специфікації написані природною мовою:
  • Algol 60 report [Архівовано 25 червня 2007 у Wayback Machine.]
  • Ada 95 reference manual [Архівовано 23 березня 2019 у Wayback Machine.]
  • Java language specification [Архівовано 26 лютого 2009 у Wayback Machine.]
  • Draft C++ standard [Архівовано 18 грудня 2018 у Wayback Machine.]
• Специфікації з використанням набору тестів:
  • Ruby's de facto community-driven specification