Trevor Jennings
Trevor is an engineer working for Altran Praxis with over 40 years of experience in the computer industry both in hardware and software roles. He has worked in many fields from safety critical systems to formula 1 racing cars and designing football scoreboards. His involvement with Ada started in 1979 during his postgraduate research at The City University in London. He assisted in creating the static analysis toolset for the first SPADE course at Southampton University and lectured on later SPADE courses. Whilst a research fellow at Southampton University between 1986 and 1989, he developed SPARK, an annotated subset of Ada specifically designed for deep static analysis for use in high-assurance systems and co-authored its first published definition with Dr Bernard Carré. Later he provided consultancy support to Program Validation Ltd. during the early days of their development of the SPARK Examiner. He has worked for Praxis for the past 4 years and for the majority of that time he has either been a member of the SPARK team developing and supporting the SPARK Toolset, or has been training and mentoring engineers new to SPARK.
What does “Frontline Support” mean to you?
Frontline support is important to the customer and to the SPARK team. It is important to the customer that we understand their problem and respond quickly with a solution or a practical work around. It is important to the SPARK team because many of the ideas for improving the SPARK Toolset or indeed extending the SPARK language come from issues raised by customers. We like to build a strong relationship with our customers.
What drew you to SPARK/Ada?
Way back in 1979 when I was doing my postgraduate research into computer aided measurement using configurable software modules I needed a programming language which provided such modularity with a strictly defined interface. Ada fitted the bill. As for SPARK, well it’s my brain child.
What’s your favorite feature of SPARK Pro Technology
The SPARK language is unambiguous and therefore you can semi-automatically prove properties of a program mathematically, for instance the proof of absence of run-time exceptions. I still marvel at this ability.
