|
|
|
|
|
|
by micronian2
2181 days ago
|
|
|
The link you provided to the SPARK user manual is a great reference. It explains how using the Ravenscar tasking profile in SPARK helps to avoid data-races and race-conditions. That, along with the ability to formally prove the absence of runtime errors and that your program satisfies various program properties and requirements are good reasons for people to seriously consider looking into using SPARK for critical parts of their software. |
|
|