921:
95:
157:
54:
898:, in SPARK. In comparing the performance of the SPARK and C implementations and after careful optimization, he managed to have the SPARK version run only about 5 to 10% slower than C. Later improvement to the Ada middle-end in GCC (implemented by Eric Botcazou of AdaCore) closed the gap, with the SPARK code matching the C in performance exactly.
247:
637:
If GNATprove is then run on the specification and corresponding body of a subprogram, it will analyse the body of the subprogram to build up a model of the information flow. This model is then compared against that which has been specified by the annotations and any discrepancies reported to the
775:
Subsequently the language was progressively extended and refined, first by
Program Validation Limited and then by Praxis Critical Systems Limited. In 2004, Praxis Critical Systems Limited changed its name to Praxis High Integrity Systems Limited. In January 2010, the company became
908:
cryptographic library in SPARK 2014. The SPARK version of the library has a complete auto-active proof of type-safety, memory-safety and some correctness properties, and retains constant-time algorithms throughout. The SPARK code is also significantly faster than TweetNaCl.
468:
SPARK utilises the strengths of Ada while trying to eliminate all its potential ambiguities and insecure constructs. SPARK programs are by design meant to be unambiguous, and their behavior is required to be unaffected by the choice of Ada
706:
or VCs. These conditions are used to establish whether certain properties hold for a given subprogram. At a minimum, the GNATprove will generate VCs to establish that all run-time errors cannot occur within a subprogram, such as:
724:
If a postcondition or any other assertion is added to a subprogram, GNATprove will also generate VCs that require the user to show that these properties hold for all possible paths through the subprogram.
1258:
456:
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
783:
In early 2009, Praxis formed a partnership with AdaCore, and released "SPARK Pro" under the terms of the GPL. This was followed in June 2009 by the SPARK GPL Edition 2009, aimed at the
553:
With SPARK 2014, contracts are added to the code to provide additional information regarding what a subprogram actually does. For example, we may alter the above specification to say:
190:
453:
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.
433:
used in systems where predictable and highly reliable operation is essential. It facilitates the development of applications that demand safety, security, or business integrity.
1248:
439:
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
1268:
1169:
67:
1263:
1243:
740:
theorem provers to discharge VCs. Use of other provers (including interactive proof checkers) is also possible through other components of the Why3 toolset.
1228:
1253:
1233:
416:
1223:
1238:
1273:
477:) and partly by introducing contracts which encode the application designer's intentions and requirements for certain components of a program.
1085:
1062:
836:
436:
Originally, there were three versions of the SPARK language (SPARK83, SPARK95, SPARK2005) based on Ada 83, Ada 95 and Ada 2005 respectively.
926:
753:
1052:
810:
The first Pro release of SPARK 2014 was announced on April 30, 2014, and was quickly followed by the SPARK 2014 GPL edition, aimed at the
116:
667:
Global => null, Depends => (X => X), Pre => X < Counter_Type'Last, Post => X = X'Old + 1;
1218:
499:
383:
321:
259:
1278:
578:
procedure does not use (neither update nor read) any global variable and that the only data item used in calculating the new value of
1010:
176:
226:
208:
138:
81:
73:
641:
These specifications can be further extended by asserting various properties that either need to hold when a subprogram is called (
1048:
703:
790:
In June 2010, Altran-Praxis announced that the SPARK programming language would be used in the software of US Lunar project
603:
Global => (In_Out => Count), Depends => (Count => (Count, X), X => null);
404:
36:
1166:
28:
769:
504:
286:
32:
186:
109:
103:
426:
400:
365:
172:
167:
856:
749:
450:
to describe the specification of components in a form that is suitable for both static and dynamic verification.
120:
473:. These goals are achieved partly by omitting some of Ada's more problematic features (such as unrestricted
430:
939:
329:
891:
860:
832:
800:
440:
682:
must be strictly less than the last possible value of its type (to ensure that the result will never
422:
254:
20:
840:
827:
SPARK has been used in several high profile safety-critical systems, covering commercial aviation (
447:
1183:
1128:
852:
266:
905:
1120:
1081:
1058:
880:
828:
733:
349:
24:
1112:
872:
683:
474:
360:
336:
480:
The combination of these approaches allows SPARK to meet its design objectives, which are:
1173:
848:
959:
728:
Under the hood, GNATprove uses the Why3 intermediate language and VC Generator, and the
634:
does not depend on any variables at all and it will be derived from constant data only.
341:
1212:
1103:
901:
NVIDIA have also adopted SPARK for the implementation of security-critical firmware.
799:
In
January 2013, Altran-Praxis changed its name to Altran which in April 2021 became
777:
649:
317:
1132:
643:
446:
The SPARK language consists of a well-defined subset of the Ada language that uses
40:
883:
demonstrator, the secunet multi-level workstation, the Muen separation kernel and
875:(Turnstile and SecureOne cross-domain solutions), the development of the original
844:
325:
312:
156:
1116:
1098:
934:
916:
890:
In August 2010, Rod
Chapman, principal engineer of Altran Praxis, implemented
1124:
804:
485:
1024:
1075:
987:
737:
470:
419:
353:
855:
system), rail (numerous signalling applications), medical (the LifeFlow
792:
275:
871:
SPARK has also been used in secure systems development. Users include
1029:
884:
876:
375:
271:
1167:
Correctness by
Construction: A Manifesto for High-Integrity Software
982:
647:) or that will hold once execution of the subprogram has completed (
246:
1198:
1151:
1188:
895:
811:
460:, and re-uses almost the entirety of the GNAT Ada 2012 front-end.
345:
1178:
1011:"Securing the Future of Safety and Security of Embedded Software"
748:
The first version of SPARK (based on Ada 83) was produced at the
784:
729:
457:
538:
by one or one thousand; or it might set some global counter to
150:
88:
47:
1146:
1203:
1156:
756:
sponsorship) by
Bernard Carré and Trevor Jennings. The name
1193:
1161:
182:
429:
programming language, intended for the development of
1054:
SPARK: The Proven
Approach to High Integrity Software
960:"SPARK - The SPADE Ada Kernel (including RavenSPARK)"
1184:
Comparison with a C specification language (Frama C)
674:is derived from itself alone, but also that before
394:
381:
371:
359:
335:
311:
285:
265:
253:
1259:Programming languages created in the 20th century
521:Consider the Ada subprogram specification below:
542:and return the original value of the counter in
171:, potentially preventing the article from being
1077:Building High Integrity Applications with SPARK
509:bounded resource (space and time) requirements.
534:In pure Ada this might increment the variable
1074:McCormick, John W.; Chapin, Peter C. (2015).
390:SPARK Pro, SPARK GPL Edition, SPARK Community
8:
653:). For example, we could say the following:
239:
589:Alternatively, the designer might specify:
82:Learn how and when to remove these messages
1249:History of computing in the United Kingdom
238:
191:reliable, independent, third-party sources
861:Vermont Technical College CubeSat project
546:; or it might do absolutely nothing with
227:Learn how and when to remove this message
209:Learn how and when to remove this message
139:Learn how and when to remove this message
904:In 2020, Rod Chapman re-implemented the
292:Community 2021 / June 1, 2021
185:by replacing them with more appropriate
102:This article includes a list of general
951:
168:too closely associated with the subject
1269:Statically typed programming languages
983:"Ada-derived Skein crypto shows SPARK"
690:will be equal to the initial value of
702:GNATprove can also generate a set of
7:
927:Free and open-source software portal
796:, expected to be completed in 2015.
571:, Depends => (X => X);
1264:Science and technology in Hampshire
1244:High Integrity Programming Language
670:This, now, specifies not only that
512:minimal runtime system requirements
1097:Ross, Philip E. (September 2005).
622:depends on the imported values of
108:it lacks sufficient corresponding
14:
1229:Algol programming language family
1179:UK's Safety-Critical Systems Club
1157:SPARK Libre (GPL) Edition website
630:, and that the exported value of
63:This article has multiple issues.
1254:Procedural programming languages
1234:Concurrent programming languages
919:
803:(following Altran's merger with
245:
166:may rely excessively on sources
155:
93:
52:
1224:Ada programming language family
859:), and space applications (the
71:or discuss these issues on the
1239:Formal specification languages
1080:. Cambridge University Press.
981:Handy, Alex (24 August 2010).
851:), air-traffic management (UK
1:
1274:Systems programming languages
618:, that the exported value of
610:will use the global variable
770:Pascal programming language
1295:
1219:Ada (programming language)
1194:Muen Kernel Public Release
1117:10.1109/MSPEC.2005.1502527
814:and academic communities.
787:and academic communities.
490:rigorous formal definition
27:framework that can run on
19:This article is about the
18:
1279:University of Southampton
1147:SPARK 2014 community site
857:ventricular assist device
750:University of Southampton
399:
389:
307:
281:
244:
894:, one of candidates for
887:block-device encrypter.
867:Security-related systems
831:series jet engines, the
711:array index out of range
574:This specifies that the
1172:30 October 2012 at the
818:Industrial applications
704:verification conditions
698:Verification conditions
614:in the same package as
458:GNAT/GCC infrastructure
431:high integrity software
123:more precise citations.
940:Java Modeling Language
839:), military aviation (
823:Safety-related systems
764:, in reference to the
686:) and that afterwards
1199:LifeFlow LVAD Project
1189:Tokeneer Project Page
837:Lockheed Martin C130J
801:Capgemini Engineering
294:; 3 years ago
714:type range violation
659:Increment (X :
606:This specifies that
595:Increment (X :
559:Increment (X :
527:Increment (X :
423:programming language
21:programming language
16:Programming language
1204:VTU CubeSat Project
1099:"The Exterminators"
841:EuroFighter Typhoon
754:Ministry of Defence
720:numerical overflow.
241:
833:ARINC ACAMS system
464:Technical overview
1152:SPARK Pro website
1087:978-1-107-65684-0
1064:978-0-9572905-1-8
1057:. Altran Praxis.
1033:. 8 October 2021.
1013:. 8 January 2020.
829:Rolls-Royce Trent
760:was derived from
517:Contract examples
410:
409:
350:Microsoft Windows
313:Typing discipline
237:
236:
229:
219:
218:
211:
149:
148:
141:
86:
25:cluster computing
1286:
1136:
1091:
1068:
1035:
1034:
1021:
1015:
1014:
1007:
1001:
1000:
998:
996:
978:
972:
971:
969:
967:
956:
929:
924:
923:
922:
873:Rockwell Collins
762:SPADE Ada Kernel
717:division by zero
693:
689:
681:
677:
673:
633:
629:
625:
621:
617:
613:
609:
585:
581:
577:
549:
545:
541:
537:
500:expressive power
493:simple semantics
475:parallel tasking
417:formally defined
302:
300:
295:
249:
242:
232:
225:
214:
207:
203:
200:
194:
159:
151:
144:
137:
133:
130:
124:
119:this article by
110:inline citations
97:
96:
89:
78:
56:
55:
48:
1294:
1293:
1289:
1288:
1287:
1285:
1284:
1283:
1209:
1208:
1174:Wayback Machine
1143:
1096:
1088:
1073:
1065:
1047:
1044:
1042:Further reading
1039:
1038:
1023:
1022:
1018:
1009:
1008:
1004:
994:
992:
980:
979:
975:
965:
963:
958:
957:
953:
948:
925:
920:
918:
915:
869:
825:
820:
746:
700:
691:
687:
679:
675:
671:
668:
631:
627:
623:
619:
615:
611:
607:
604:
583:
579:
575:
572:
547:
543:
539:
535:
532:
531:Counter_Type);
519:
466:
384:implementations
303:
298:
296:
293:
233:
222:
221:
220:
215:
204:
198:
195:
180:
160:
145:
134:
128:
125:
115:Please help to
114:
98:
94:
57:
53:
44:
17:
12:
11:
5:
1292:
1290:
1282:
1281:
1276:
1271:
1266:
1261:
1256:
1251:
1246:
1241:
1236:
1231:
1226:
1221:
1211:
1210:
1207:
1206:
1201:
1196:
1191:
1186:
1181:
1176:
1164:
1159:
1154:
1149:
1142:
1141:External links
1139:
1138:
1137:
1093:
1092:
1086:
1070:
1069:
1063:
1043:
1040:
1037:
1036:
1016:
1002:
991:. BZ Media LLC
973:
950:
949:
947:
944:
943:
942:
937:
931:
930:
914:
911:
868:
865:
849:AerMacchi M346
824:
821:
819:
816:
768:subset of the
745:
742:
722:
721:
718:
715:
712:
699:
696:
663:Counter_Type)
655:
650:postconditions
599:Counter_Type)
591:
563:Counter_Type)
555:
523:
518:
515:
514:
513:
510:
507:
502:
497:
494:
491:
488:
465:
462:
408:
407:
397:
396:
392:
391:
387:
386:
379:
378:
373:
369:
368:
363:
357:
356:
342:Cross-platform
339:
333:
332:
315:
309:
308:
305:
304:
291:
289:
287:Stable release
283:
282:
279:
278:
269:
263:
262:
260:Multi-paradigm
257:
251:
250:
235:
234:
217:
216:
163:
161:
154:
147:
146:
129:September 2010
101:
99:
92:
87:
61:
60:
58:
51:
15:
13:
10:
9:
6:
4:
3:
2:
1291:
1280:
1277:
1275:
1272:
1270:
1267:
1265:
1262:
1260:
1257:
1255:
1252:
1250:
1247:
1245:
1242:
1240:
1237:
1235:
1232:
1230:
1227:
1225:
1222:
1220:
1217:
1216:
1214:
1205:
1202:
1200:
1197:
1195:
1192:
1190:
1187:
1185:
1182:
1180:
1177:
1175:
1171:
1168:
1165:
1163:
1160:
1158:
1155:
1153:
1150:
1148:
1145:
1144:
1140:
1134:
1130:
1126:
1122:
1118:
1114:
1110:
1106:
1105:
1104:IEEE Spectrum
1100:
1095:
1094:
1089:
1083:
1079:
1078:
1072:
1071:
1066:
1060:
1056:
1055:
1050:
1046:
1045:
1041:
1032:
1031:
1026:
1020:
1017:
1012:
1006:
1003:
990:
989:
984:
977:
974:
961:
955:
952:
945:
941:
938:
936:
933:
932:
928:
917:
912:
910:
907:
902:
899:
897:
893:
888:
886:
882:
878:
874:
866:
864:
862:
858:
854:
850:
846:
842:
838:
834:
830:
822:
817:
815:
813:
808:
806:
802:
797:
795:
794:
788:
786:
781:
779:
778:Altran Praxis
773:
771:
767:
763:
759:
755:
751:
743:
741:
739:
735:
731:
726:
719:
716:
713:
710:
709:
708:
705:
697:
695:
685:
666:
662:
658:
654:
652:
651:
646:
645:
644:preconditions
639:
635:
602:
598:
594:
590:
587:
570:
567:Global =>
566:
562:
558:
554:
551:
530:
526:
522:
516:
511:
508:
506:
505:verifiability
503:
501:
498:
495:
492:
489:
487:
483:
482:
481:
478:
476:
472:
463:
461:
459:
454:
451:
449:
444:
442:
437:
434:
432:
428:
425:based on the
424:
421:
418:
414:
406:
402:
398:
395:Influenced by
393:
388:
385:
380:
377:
374:
370:
367:
364:
362:
358:
355:
351:
347:
343:
340:
338:
334:
331:
327:
323:
319:
316:
314:
310:
306:
290:
288:
284:
280:
277:
273:
270:
268:
264:
261:
258:
256:
252:
248:
243:
231:
228:
213:
210:
202:
192:
188:
184:
178:
174:
170:
169:
164:This article
162:
158:
153:
152:
143:
140:
132:
122:
118:
112:
111:
105:
100:
91:
90:
85:
83:
76:
75:
70:
69:
64:
59:
50:
49:
46:
42:
38:
34:
30:
26:
22:
1111:(9): 36–41.
1108:
1102:
1076:
1053:
1049:Barnes, John
1028:
1019:
1005:
993:. Retrieved
986:
976:
964:. Retrieved
954:
903:
900:
889:
879:CA, the NSA
870:
826:
809:
798:
791:
789:
782:
774:
765:
761:
757:
747:
727:
723:
701:
669:
664:
660:
656:
648:
642:
640:
636:
605:
600:
596:
592:
588:
573:
568:
564:
560:
556:
552:
533:
528:
524:
520:
479:
467:
455:
452:
445:
441:verification
438:
435:
412:
411:
223:
205:
196:
181:Please help
165:
135:
126:
107:
79:
72:
66:
65:Please help
62:
45:
41:Apache Spark
1025:"SPARKNaCl"
853:NATS iFACTS
845:Harrier GR9
376:About SPARK
121:introducing
1213:Categories
946:References
935:Z notation
694:plus one.
678:is called
330:nominative
299:2021-06-01
183:improve it
173:verifiable
104:references
68:improve it
23:. For the
1125:0018-9235
995:31 August
962:. AdaCore
906:TweetNaCl
805:Capgemini
752:(with UK
676:Increment
657:procedure
616:Increment
608:Increment
593:procedure
576:Increment
557:procedure
525:procedure
486:soundness
448:contracts
267:Developer
187:citations
74:talk page
1170:Archived
1133:26369398
1051:(2012).
988:SD Times
913:See also
881:Tokeneer
738:Alt-Ergo
684:overflow
586:itself.
550:at all.
496:security
484:logical
471:compiler
420:computer
354:Mac OS X
255:Paradigm
199:May 2014
966:30 June
793:CubeSat
744:History
443:tools.
372:Website
361:License
297: (
276:AdaCore
177:neutral
117:improve
1162:Altran
1131:
1123:
1084:
1061:
1030:GitHub
885:Genode
877:MULTOS
835:, the
736:, and
661:in out
638:user.
597:in out
561:in out
529:in out
405:Eiffel
382:Major
322:strong
318:static
272:Altran
106:, but
39:, see
37:Python
35:, and
1129:S2CID
896:SHA-3
892:Skein
812:FLOSS
766:SPADE
758:SPARK
624:Count
620:Count
612:Count
415:is a
413:SPARK
366:GPLv3
346:Linux
240:SPARK
29:Scala
1121:ISSN
1082:ISBN
1059:ISBN
997:2010
968:2021
785:FOSS
730:CVC4
665:with
626:and
601:with
569:null
565:with
326:safe
274:and
175:and
33:Java
1113:doi
863:).
807:).
582:is
427:Ada
401:Ada
189:to
1215::
1127:.
1119:.
1109:42
1107:.
1101:.
1027:.
985:.
847:,
843:,
780:.
772:.
734:Z3
732:,
403:,
352:,
348:,
344::
337:OS
328:,
324:,
320:,
77:.
31:,
1135:.
1115::
1090:.
1067:.
999:.
970:.
692:X
688:X
680:X
672:X
632:X
628:X
584:X
580:X
548:X
544:X
540:X
536:X
301:)
230:)
224:(
212:)
206:(
201:)
197:(
193:.
179:.
142:)
136:(
131:)
127:(
113:.
84:)
80:(
43:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
