You've already forked Compile_And_Prove_Demo
mirror of
https://github.com/AdaCore/Compile_And_Prove_Demo.git
synced 2026-02-12 12:45:02 -08:00
7 lines
340 B
YAML
7 lines
340 B
YAML
name: Sensor Average
|
|
description: >
|
|
This shows basic use of fixed-point types in SPARK (real types with a fixed
|
|
precision contrary to floating-point types) and variables with memory-mapped
|
|
addresses for sensors. In the initial version, the postcondition of a local
|
|
function cannot be proved due to missing parentheses in an expression.
|