Praxis Critical System’s Approach and the SPARK Language

Example


•	Initializes the array A to 0.

•	3 VCs generated

•	These VCs require the proof checker