Bernard Carré is a computing figure credited, together with Trevor Jennings, with producing the first version of the SPARK programming language. That first version was based on Ada 83 and was made at the University of Southampton in 1987, with sponsorship from the UK Ministry of Defence. The name SPARK was derived from SPADE Ada Kernel, in reference to the SPADE subset of the Pascal programming language. SPARK is a well-defined subset of Ada that uses contracts to describe the specification of components in a form suitable for both static and dynamic verification. The language was afterwards extended and refined by Program Validation Limited and then by Praxis Critical Systems, and in 2009 Praxis partnered with AdaCore to release SPARK Pro under the GPL. The article cited here says nothing more about his life.
Facts
Contribution Kind Connections
In Field
Source SPARK (programming language) (Wikipedia)
Sources
1. SPARK (programming language) (Wikipedia)
History, first version of the language
The first version of SPARK (based on Ada 83) was produced at the university, with UK Ministry of Defence sponsorship, by Bernard Carré and Trevor Jennings.
In Group: Programming Language Designers, History, first version
The first version of SPARK (based on Ada 83) was produced at the university, with UK Ministry of Defence sponsorship, by Bernard Carré and Trevor Jennings.
In Field: Formal Methods, Lead, verification
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.
View the SourceReader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.
Sign in to dispute this or suggest a correction.