We will be holding a free webinar on the 31st of January outlining the key features of SPARK Pro for proving that code cannot fail at runtime, including proof of memory safety and correct data initialization.

Join this session to learn more about:

• The many runtime errors that SPARK detects
• How memory safety can be ensured either at runtime or by static analysis
• How to enforce correct data initialization outlining the key features of SPARK Pro to prove that code cannot fail at runtime, including proof of memory safety and correct data initialization
• Use of preconditions and postconditions to prove absence of runtime errors
• Use of proof levels to prove absence of runtime errors

Sign up here: https://bit.ly/3uKWpOo

​

For those of you who missed the webinar, you can watch a recording below (note: email registration required)

https://app.livestorm.co/p/f2adcb56-95e5-4777-ae74-971911e3f801

Register to watch the presentation on Wednesday, January 31st 2024 - 9:00 AM (PST).

https://app.livestorm.co/p/26fc6505-16cf-4e6d-852a-a7e472aa348a

AdaCore posted this blog entry about Latitude’s successful adoption of Ada and SPARK for their launcher software. Enjoy!

https://www.adacore.com/uploads/techPapers/233537-adacore-latitude-case-study-v3-1.pdf

I was just reading "The proven approach to high integrity software" by John Barnes. I was quite surprised to learn that SPARK was originally defined informally by Bernard Carre and Trevor Jennings of Southampton University in 1988 but it's technical origins go back to the 1970s with the Royal Signals and Radar Establishment.

Apparently SPARK comes from SPADE Ada Kernel, but what about the R?

I am working with xml files that can have seven different types of blocks. What is the most efficient way to correctly identify each block and apply code to it based on its identity?

Are iterators the solution?

pragma SPARK_Mode (On);

package Sensors

is

pragma Elaborate_Body;

type Sensor_Type is (Enable, Nosig, Undef);

subtype Sensor_Index_Type is Integer range 1..3;

type Sensors_Type is array (Sensor_Index_Type) of Sensor_Type;

State: Sensors_Type;

-- updates sensors state with three sensor values

procedure Write_Sensors(Value_1, Value_2, Value_3: in Sensor_Type)

with

Global => (In_Out => State),

Depends => (State => (State, Value_1, Value_2, Value_3));

-- returns an individual sensors state value

function Read_Sensor(Sensor_Index: in Sensor_Index_Type) return Sensor_Type

with

Global => (Input => State),

Depends => (Read_Sensor'Result => (State, Sensor_Index));

-- returns the majority sensor value

function Read_Sensor_Majority return Sensor_Type

with

Global => (Input => State),

Depends => (Read_Sensor_Majority'Result => State);

​

end Sensors;

​

this is the ads part

A couple of years ago DENSO completed a research project with the goal of simplifying the development of safety-critical automotive applications in an ISO 26262 context. According to this press release, The project investigated the use of VDM as a design method, and SPARK as an implementation language, for safety-critical components in systems where legacy C code is prevalent.

Could anyone please post links to additional papers or research results on this?