SPARK

Website: About SPARK

Spark este un limbaj de programare computerizat definit formal bazat pe limbajul de programare ADA, destinat dezvoltării de software de înaltă integritate utilizat în sistemele în care este esențială o funcționare previzibilă și extrem de fiabilă.

Acesta facilitează dezvoltarea aplicațiilor care necesită siguranță, securitate sau integritate a afacerii.

Inițial, au existat trei versiuni ale limbajului Spark (Spark83, Spark95, Spark2005) pe baza ADA 83, ADA 95 și, respectiv, ADA 2005.

O a patra versiune a Language Spark, Spark 2014, bazată pe ADA 2012, a fost lansată pe 30 aprilie 2014.

Spark 2014 este o re-proiectare completă a limbajului și a instrumentelor de verificare de susținere.

Limbajul Spark constă dintr-un subset bine definit al limbajului ADA care folosește contracte pentru a descrie specificația componentelor într-o formă adecvată atât pentru verificarea statică, cât și pentru cele dinamice.

În Spark83/95/2005, contractele sunt codificate în comentarii ADA și astfel sunt ignorate de orice compilator ADA standard, dar sunt procesate de „examinatorul” Spark și instrumentele asociate.

Spark 2014, în schimb, folosește sintaxa „aspect” încorporată de ADA 2012 pentru a exprima contracte, aducându-le în miezul limbii.

Principalul instrument pentru Spark 2014 (GNATPROVE) se bazează pe infrastructura GNAT/GCC și reutilizează aproape întreaga front-end GNAT ADA 2012.