This HTML5 document contains 286 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Subject Item

n2:

rdf:type

yago:Instrumentality103575240 wd:Q34770 wd:Q35120 yago:WikicatFormalSpecificationLanguages wd:Q312466 wd:Q315 wd:Q7397 wd:Q17376908 wd:Q853614 wd:Q20811739 owl:Thing wd:Q17537576 wd:Q629206 wd:Q223557 dbo:ProgrammingLanguage yago:WikicatProgrammingLanguagesCreatedInThe20thCentury wd:Q16686448 schema:Language dbo:Language wd:Q488383 wd:Q11028 yago:WikicatFormalMethodsTools yago:PhysicalEntity100001930 yago:Object100002684 wd:Q28877 wd:Q192161 wd:Q9143 wd:Q2424752 yago:Whole100003553 wd:Q386724 wd:Q7184903 yago:Abstraction100002137 yago:Implement103563967 yago:Tool104451818 yago:Communication100033020 yago:Language106282651 yago:Artifact100021939 wd:Q15621286 yago:WikicatProgrammingLanguages yago:ArtificialLanguage106894544 yago:ProgrammingLanguage106898352 wd:Q676202

rdfs:label

SPARK SPARK (informatyka) SPARK (programming language) SPARK SPARK (язык программирования)

rdfs:comment

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. SPARK es un lenguaje de programación especialmente diseñado para . Es un subconjunto anotado de Ada desarrollado por la empresa británica Praxis High Integrity Systems, Inc Archivado el 10 de julio de 2006 en Wayback Machine. que elimina ciertas características del lenguaje consideradas peligrosas en este tipo de sistemas (como las excepciones o la sobrecarga de operadores), y que añade anotaciones formales para realizar automáticamente análisis de flujo de datos y de información. SPARK (SPADE Ada Kernel) — формально определённый язык программирования, являющийся подмножеством Ады, предназначен для разработки верифицированного программного обеспечения высокого . SPARK позволяет создавать приложения, которые обладают предсказуемым поведением и обеспечивают высокую надёжность. SPARK используется в авиации (реактивные двигатели Rolls-Royce Trent, самолёты Eurofighter Typhoon и Бе-200, система UK NATS iFACTS) и для разработки космических систем (РН Вега, множество спутников). Также его применяют для разработки систем шифрования и кибербезопасности. SPARK是一种安全的、经正式定义的编程语言。它被设计用来支持一些安全或商业集成为关键因素的应用软件的设计。SPARK有基于Ada 83和Ada 95的版本。最新版本RavenSPARK包含了Ravenscar Tasking Profile来支持高度集成应用中的同步。SPARK的正式和明确的定义使得多种静态分析技术在SPARK源代码的应用中成为可能。 SPARK Ada, SPARK 95 – podzbiór języka Ada zaprojektowany w celu tworzenia kodu wolnego od błędów dla zastosowania w systemach mission-critical. Język został stworzony w 1999 roku przez brytyjską firmę na bazie podobnego podzbioru języka SPADE Pascal oraz języka Ada 95. Język jest zaprojektowany w taki sposób, aby możliwa była formalna analiza oraz dowodzenie poprawności kodu. Usunięte zostały z niego wszelkie dwuznaczności, elementy sprzyjające nieprzewidzianym przepływom danych (np. wyjątki), wprowadzono mechanizm formalnych komentarzy (formal comments, annotations). W celu umożliwienia silnej weryfikacji poprawności kodu wprowadzono precyzyjne specyfikacje wejścia i wyjścia poszczególnych procedur. Ochronę stabilności zapewnia m.in. wewnętrzna kontrola liczby iteracji oraz czasu wykonan

owl:sameAs

dbpedia-zh:SPARK n30: n31: n33: n34:3DoQR n2: dbpedia-es:SPARK n38:01qplz wd:Q3493345 n56:

foaf:name

SPARK

foaf:homepage

n10:about-spark

dbp:name

SPARK

foaf:topic

dbr:Lunar_IceCube dbr:History_of_software dbr:Automated_theorem_proving dbr:IBM_Watson_Studio dbr:Vermont_Lunar_CubeSat dbr:RavenSPARK dbr:Frama-C dbr:SPARK_Language dbr:SPARK_Examiner dbr:SPARK_programming_language dbr:SPARK_Toolset dbr:SPARK_language dbr:SPARK_Programming_Language dbr:Spark_language dbr:Alt-Ergo n29: dbr:Formal_methods dbr:Spark_programming_language dbr:List_of_programming_languages dbr:Halting_problem dbr:Ravenscar_profile dbr:Design_by_contract dbr:GNAT n47: dbr:Formal_verification n49:this dbr:SPADE_Ada_Kernel n52: dbr:Ada_Spark n57:SPARK n57:Spark n43: dbr:Altran_Praxis dbr:Timeline_of_programming_languages n62: n44: dbr:Spark n63:Class_Q_--_Science n65: dbr:Generational_list_of_programming_languages dbr:Extended_static_checking n35: dbr:Satisfiability_modulo_theories

foaf:depiction

n51:jpg

wdrs:describedby

n18:Tool104451818 n18:Implement103563967 n27:Mac_OS_X n18:Language106282651 n27:Precondition n27:GNU_General_Public_License n27:Cross-platform n60:Microsoft_Windows n61: n60:Programming_language n67:ArtificialLanguage106894544 n68: n27:Computer

foaf:page

n10:about-spark

dbp:implementations

SPARK Pro, SPARK GPL Edition, SPARK Community

dbp:influencedBy

n32: n44:

dbp:latestReleaseDate

2021-06-01

dbp:latestReleaseVersion

Community 2021

dbp:operatingSystem

dbr:Microsoft_Windows dbr:Mac_OS_X dbr:Cross-platform dbr:Linux

dbp:paradigm

dbr:Multi-paradigm_programming_language

dbp:typing

dbr:Static_typing dbr:Nominative_type_system dbr:Strongly_typed_programming_language dbr:Type_safety

dct:subject

dbc:High_Integrity_Programming_Language dbc:Procedural_programming_languages dbc:Statically_typed_programming_languages dbc:Ada_programming_language_family dbc:Concurrent_programming_languages dbc:Science_and_technology_in_Hampshire dbc:Systems_programming_languages n42: dbc:History_of_computing_in_the_United_Kingdom dbc:Algol_programming_language_family dbc:Formal_specification_languages dbc:Programming_languages_created_in_the_20th_century dbc:University_of_Southampton

dbo:wikiPageID

291874

dbo:wikiPageRevisionID

1120618969

dbo:wikiPageWikiLink

dbr:NATS_iFACTS dbr:ARINC_ACAMS_system dbr:MULTOS dbr:Static_typing dbc:Programming_languages_created_in_the_20th_century dbr:Genode dbr:Sha-3 n21: dbr:Lockheed_Martin_C-130J_Super_Hercules dbc:Statically_typed_programming_languages dbc:High_Integrity_Programming_Language dbc:Procedural_programming_languages dbr:Ventricular_assist_device dbr:Pascal_programming_language dbr:Linux n28: dbr:Aermacchi_M-346 dbr:Rolls-Royce_Trent dbr:FLOSS dbr:CVC4 dbr:Verification_condition_generator dbc:Science_and_technology_in_Hampshire dbr:AdaCore dbr:Z3_Theorem_Prover dbr:High_integrity_software dbr:Mac_OS_X dbc:Concurrent_programming_languages dbr:Rockwell_Collins n36: dbr:Software_verification dbr:FOSS dbc:Ada_programming_language_family dbc:Systems_programming_languages dbr:Type_safety dbr:Cross-platform dbr:GNAT n39: dbr:Strongly_typed_programming_language n42: dbr:Multi-paradigm_programming_language dbc:History_of_computing_in_the_United_Kingdom dbr:Altran_Praxis dbr:CubeSat dbr:Computer n43: n45: dbr:Compiler dbc:Algol_programming_language_family dbr:Java_Modeling_Language dbr:Microsoft_Windows dbr:Z_notation dbr:University_of_Southampton n44: dbr:Vermont_Lunar_CubeSat dbc:Formal_specification_languages dbr:Formal_semantics_of_programming_languages dbr:IEEE_Spectrum dbr:Altran dbr:Programming_language dbr:Cluster_computing dbr:Precondition dbr:Eurofighter_Typhoon dbr:Alt-Ergo n59:jpg dbr:GNU_General_Public_License dbr:Nominative_type_system dbr:Postcondition dbr:Capgemini n32: dbr:Integer_overflow dbc:University_of_Southampton dbr:Verification_and_validation dbr:Capgemini_Engineering dbr:Harrier_GR9 dbr:Tokeneer n69: dbr:TweetNaCl dbr:Soundness dbr:Task_parallelism

dbo:wikiPageExternalLink

n11:the-exterminators n10:about-spark n12:html n14:org n22:ch n23:9781107656840 n24: n25: n26:edu n41:pdf n50: n58: n64: n66:SPARK__The_Proven_Approach_to_High_Integrity_Software n10:tokeneer n46:pdf

foaf:isPrimaryTopicOf

n35:

prov:wasDerivedFrom

n55:0

dbo:abstract

SPARK是一种安全的、经正式定义的编程语言。它被设计用来支持一些安全或商业集成为关键因素的应用软件的设计。SPARK有基于Ada 83和Ada 95的版本。最新版本RavenSPARK包含了Ravenscar Tasking Profile来支持高度集成应用中的同步。SPARK的正式和明确的定义使得多种静态分析技术在SPARK源代码的应用中成为可能。 SPARK es un lenguaje de programación especialmente diseñado para . Es un subconjunto anotado de Ada desarrollado por la empresa británica Praxis High Integrity Systems, Inc Archivado el 10 de julio de 2006 en Wayback Machine. que elimina ciertas características del lenguaje consideradas peligrosas en este tipo de sistemas (como las excepciones o la sobrecarga de operadores), y que añade anotaciones formales para realizar automáticamente análisis de flujo de datos y de información. SPARK Ada, SPARK 95 – podzbiór języka Ada zaprojektowany w celu tworzenia kodu wolnego od błędów dla zastosowania w systemach mission-critical. Język został stworzony w 1999 roku przez brytyjską firmę na bazie podobnego podzbioru języka SPADE Pascal oraz języka Ada 95. Język jest zaprojektowany w taki sposób, aby możliwa była formalna analiza oraz dowodzenie poprawności kodu. Usunięte zostały z niego wszelkie dwuznaczności, elementy sprzyjające nieprzewidzianym przepływom danych (np. wyjątki), wprowadzono mechanizm formalnych komentarzy (formal comments, annotations). W celu umożliwienia silnej weryfikacji poprawności kodu wprowadzono precyzyjne specyfikacje wejścia i wyjścia poszczególnych procedur. Ochronę stabilności zapewnia m.in. wewnętrzna kontrola liczby iteracji oraz czasu wykonania procedur. Język posiada szereg rozszerzeń przeznaczonych do obsługi urządzeń fizycznych działających w czasie rzeczywistym np. sensorów. Programy napisane w języku SPARK Ada są kompatybilne ze standardowym językiem Ada. Funkcje formalnej analizy poprawności są relizowane przez dodatkowe narzędzia (SPARK Examiner) bazujące głównie na rozszerzeniach jakimi są formalne komentarze. Przykład fragmentu kodu z formalnymi komentarzami SPARK: procedure Increment (X : in out Counter_Type);--# derives X from X;--# pre X < Counter_Type'Last;--# post X = X~ + 1; Komentarze te precyzyjnie określają do jakich zmiennych globalnych odwołuje się dana funkcja oraz w jaki sposób wpływa ona na wartość zmiennej X (może być tylko większa o 1, nie mniejsza, ani nie równa początkowej wartości) oraz jaka musi być początkowa wartość zmiennej X (mniejsza od największej dopuszczalnej wartości Counter_Type). Deklaracje te stanowią podstawę dla formalnej weryfikacji kodu funkcji przez SPARK Examiner, który sprawdza czy wynik działania tego kodu będzie zgodny z deklaracjami formalnymi. 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 (SPADE Ada Kernel) — формально определённый язык программирования, являющийся подмножеством Ады, предназначен для разработки верифицированного программного обеспечения высокого . SPARK позволяет создавать приложения, которые обладают предсказуемым поведением и обеспечивают высокую надёжность. Версии языка SPARK связаны с версиями Ады и разделены на два поколения: SPARK 83, SPARK 95 и SPARK 2005 (Ada 83, Ada 95 и Ada 2005 соответственно) относят к первому поколению, а SPARK 2014 (Ada 2012) — ко второму. Это обусловлено тем, что первоначально для указания спецификаций и контрактов использовались комментарии, но, начиная с Ada 2012, для этого стал применяться появившийся в языке механизм аспектов. Это привело к полной переработке всего инструментария языка и появлению нового верификатора GNATprove. SPARK используется в авиации (реактивные двигатели Rolls-Royce Trent, самолёты Eurofighter Typhoon и Бе-200, система UK NATS iFACTS) и для разработки космических систем (РН Вега, множество спутников). Также его применяют для разработки систем шифрования и кибербезопасности.

dbo:license

dbr:GNU_General_Public_License

dbo:thumbnail

n48:300

dbp:date

2012-10-30

dbp:license

dbr:GNU_General_Public_License

dbp:logo

250

dbp:url

n46:pdf

dbp:website

n10:about-spark

dbp:wordnet_type

n53:synset-software-noun-1 n53:synset-programming_language-noun-1

dbp:developer

Altran and AdaCore

dbo:influencedBy

n32: n44:

dbo:latestReleaseVersion

Community 2021

dbo:latestReleaseDate

2021-06-01

dbo:developer

dbr:Altran dbr:AdaCore

dbo:wikiPageLength

14249

dbp:wikiPageUsesTemplate

dbt:Citation_needed dbt:Short_description dbt:Start_date_and_age dbt:Cite_journal dbt:Use_dmy_dates dbt:About dbt:Webarchive dbt:Authority_control dbt:More_footnotes_needed dbt:Portal dbt:Infobox_programming_language dbt:Third-party dbt:Reflist dbt:Multiple_issues dbt:Cite_book