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

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

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

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

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

— Корнеліс Костер, [2]

Форми

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

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

Синтаксис

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

Семантика

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Набір тестів

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

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

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

Посилання

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

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

Примітки
  1. Announcing a specification for PHP, 30 липня 2014, Joel Marcey
  2. A Shorter History of Algol68. Архів оригіналу за 10 серпня 2006. Процитовано 15 вересня 2006.
  3. Milner, R.; M. Tofte; R. Harper; D. MacQueen (1997). The Definition of Standard ML (Revised). MIT Press. ISBN 0-262-63181-4.
  4. Kelsey, Richard; William Clinger; Jonathan Rees (February 1998). Section 7.2 Formal semantics. Revised5 Report on the Algorithmic Language Scheme. Процитовано 9 червня 2006.
  5. Jones, D. (2008). Forms of language specification. Процитовано 23 червня 2012.
  6. William Pugh. The Java Memory Model is Fatally Flawed. Concurrency: Practice and Experience 12(6):445-455, August 2000
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.