Кіріспе
Бағдарламалау тілі
SPARK бағдарламалау тілі – Ada бағдарламалау тіліне негізделген, болжамды және жоғары сенімді жұмыс істеуі қажетті жүйелерде қолданылатын жоғары тұтастығы бар бағдарламалық жасақтаманы әзірлеуге арналған, ресми түрде анықталған компьютерлік бағдарламалау тілі. Ол қауіпсіздік, қорғау немесе бизнес тұтастығы талаптарын қанағаттандыратын қосымшаларды әзірлеуді жеңілдетеді. Алғашқыда SPARK тілінің үш нұсқасы болды (SPARK83, SPARK95, SPARK2005), олар сәйкесінше Ada 83, Ada 95 және Ada 2005 тілдеріне негізделген. SPARK тілінің төртінші нұсқасы, SPARK 2014, Ada 2012 негізінде 2014 жылдың 30 сәуірінде жарияланды. SPARK 2014 – бұл тілдің толық қайта жаңартылуы және оны қолдайтын тексеру құралдары. SPARK тілі – компоненттердің сипаттамасын статикалық және динамикалық тексеруге ыңғайлы форматта беру үшін келісімшарттарды пайдаланатын Ada тілінің жақсы анықталған кіші жиынтығынан тұрады. SPARK83/95/2005 нұсқаларында келісімшарттар Ada түсініктемелерінде кодталған, сондықтан кез келген стандартты Ada компиляторы оларды назарға алмайды, бірақ SPARK "Examiner" және оған қоса берілген құралдар оларды өңдейді. SPARK 2014, керісінше, келісімшарттарды білдіру үшін Ada 2012 тілінің енгізілген "аспект" синтаксисін пайдаланады, осылайша оларды тілдің негізгі бөлігіне енгізеді. SPARK 2014-тің негізгі құралы (GNATprove) GNAT/GCC инфрақұрылымына негізделген және GNAT Ada 2012 алдыңғы бөлігінің дерлік барлық мүмкіндіктерін қайта пайдаланады.
the programming language
SPARK is a formally defined computer programming language based on the Ada programming language, intended for the development of high integrity software used in systems where predictable and highly reliable operation is essential. It facilitates the development of applications that demand safety, security, or business integrity. Originally, there were three versions of the SPARK language (SPARK83, SPARK95, SPARK2005) based on Ada 83, Ada 95 and Ada 2005 respectively. A fourth version of the SPARK language, SPARK 2014, based on Ada 2012, was released on April 30, 2014. SPARK 2014 is a complete re design of the language and supporting verification tools. The SPARK language consists of a well defined subset of the Ada language that uses contracts to describe the specification of components in a form that is suitable for both static and dynamic verification. In SPARK83/95/2005, the contracts are encoded in Ada comments and so are ignored by any standard Ada compiler, but are processed by the SPARK "Examiner" and its associated tools. SPARK 2014, in contrast, uses Ada 2012's built in "aspect" syntax to express contracts, bringing them into the core of the language. The main tool for SPARK 2014 (GNATprove) is based on the GNAT/GCC infrastructure, and re uses almost the entirety of the GNAT Ada 2012 front end.
Тарих
SPARK-тың алғашқы нұсқасы (Ada 83-ге негізделген) Саутгемптон университетінде (Ұлыбритания Қорғаныс министрлігінің қолдауымен) Бернард Карре мен Тревор Дженнингс жасады. SPARK атауы SPADE Ada Kernel-ден шығарылған, бұл Pascal бағдарламалау тілінің SPADE кіші жиынтығына сілтеме еді. Кейін тіл біртіндеп кеңейтіліп, жетілдірілді, бірінші Program Validation Limited, содан кейін Praxis Critical Systems Limited компаниялары арқылы. 2004 жылы Praxis Critical Systems Limited компаниясы өзінің атауын Praxis High Integrity Systems Limited деп өзгертті. 2010 жылдың қаңтар айында компания Altran Praxis болып қайта аталды. 2009 жылдың басында Praxis, AdaCore компаниясымен серіктестікке келісіп, GPL шарттары бойынша "SPARK Pro" бағдарламасын жариялады. 2009 жылдың маусымында FOSS және академиялық қауымдастықтарға бағытталған SPARK GPL Edition 2009 нұсқасы шықты. 2010 жылдың маусым айында Altran Praxis компаниясы SPARK бағдарламалау тілінің 2015 жылы аяқталуы күтілетін АҚШ-тың Ай жобасы CubeSat бағдарламалық қамтамасыздандыруында қолданылатынын хабарлады. 2013 жылдың қаңтар айында Altran Praxis өзінің атын Altran деп өзгертіп, 2021 жылдың сәуірінде Altran-ның Capgemini компаниясымен бірігуінен кейін Capgemini Engineering болып қайта аталды. SPARK 2014 Pro-ның алғашқы нұсқасы 2014 жылдың 30 сәуірінде жарияланды, одан кейін FLOSS және академиялық қауымдастықтарға арналған SPARK 2014 GPL нұсқасы тез арада шықты.
Қауіпсіздікке байланысты жүйелер
SPARK бірнеше жоғары маңызды қауіпсіздікке қатысты жүйелерде қолданылды, олардың ішінде коммерциялық авиация (Rolls Royce Trent сериялы реактивті қозғалтқыштар, ARINC ACAMS жүйесі, Lockheed Martin C130J), әскери авиация (EuroFighter Typhoon, Harrier GR9, AerMacchi M346), әуе трафигін басқару (UK NATS iFACTS жүйесі), теміржол (көптеген сигнализация қолданбалары), медицина (LifeFlow қарыншалық көмек құрылғысы) және ғарыш саласындағы қолданбалар (Вермонт техникалық колледжінің CubeSat жобасы) бар.
Қауіпсіздікке байланысты жүйелер
SPARK қауіпсіз жүйелерді әзірлеуде де қолданылды. Оны пайдаланушылардың арасында Rockwell Collins (Turnstile және SecureOne кросс-домендік шешімдері), түпнұсқа MULTOS CA, NSA Tokeneer демонстрациялық нұсқасы, secunet көп деңгейлі жұмыс станциясы, Muen бөлу ядросы және Genode блок құрылғысы шифрлаушысы бар. 2010 жылдың тамызында Altran Praxis бас инженері Род Чэпман SPARK-та SHA-3 үміткерлерінің бірі – Skein алгоритмін іске қосты. SPARK және C нұсқаларын салыстырып, мұқият оңтайландырудан кейін ол SPARK нұсқасын C нұсқасынан шамамен 5-10% ғана баяурақ жұмыс істеуге қол жеткізді. Кейіннен GCC-дегі Ada аралық бөлігіне (AdaCore-дың Эрик Ботказу жүзеге асырған) енгізілген жақсартулар бұл айырмашылықты жойды, SPARK коды C кодымен бірдей өнімділік көрсетті. NVIDIA да қауіпсіздікке маңызды бағдарламалық құралдарды іске асыру үшін SPARK-ты пайдаланды. 2020 жылы Род Чэпман TweetNaCl криптографиялық кітапханасын SPARK 2014 платформасында қайта іске қосты. Кітапхананың SPARK нұсқасы типтік қауіпсіздік, жад қауіпсіздігі және дұрыстық қасиеттерін автоматты түрде толық растайды, сонымен қатар алгоритмдердің уақыт бойынша тұрақтылығын сақтайды. SPARK коды TweetNaCl-ге қарағанда едәуір жылдам.