<commit_before># Verifying numerical SPARK Ada programs using PolyPaver 

TODO: a few sentences of introduction

## Overview of the example programs

### peak

*Main procedure*: PeakUnit  
*Input*: real values Y1, Y2, Y3  
*Output*: the peak value of the *quadratic* interpolation of (-1,Y1), (0,Y2), (1,Y3)

### sqrt

*Main procedure*: Sqrt  
*Input*: real value X  
*Output*: the square root of X

### erfriemann

*Main procedure*: erfRiemann  
*Input*: real value X and integer n  
*Output*: a Riemann sum over n segments, approximating the value of the Gaussian error function for X

## How to write SPARK programs that can be verified using PolyPaver

TODO: 
* List replacements for Ada FP operations and functions.  
* State that in annotations, numerical operations retain their exact meaning.
* List annotation functions understood by polypaver (such as such as polypaver.exact.sqrt). 

## Generation of verification conditions (VCs):

In the program main folder, execute:

    > spark @peak
    > sparksimp
<commit_msg>Added attempts at some of the TODOs in the SPARK/README.md file.<commit_after># Verifying numerical SPARK Ada programs using PolyPaver 

PolyPaver provides facilities for automatically proving SPARK generated verification conditions (VCs) that make up correctness theorems for SPARK Ada prorams. The verification approach relies on the SPAR toolset for VC generation and simplification. The resulting correctness theorems genrally comprise the set of numerically nontrivial sub-theorems encoding exception freedom and (optionally) accuracy properties. Below follows a brief introduction to the method by which VCs may be derived that PolyPaver can process and a procedure for working with the options provided by PolyPaver to guide and control the proof effort. 

## Overview of the example programs

### peak

*Main procedure*: PeakUnit  
*Input*: real values Y1, Y2, Y3  
*Output*: the peak value of the *quadratic* interpolation of (-1,Y1), (0,Y2), (1,Y3)

### sqrt

*Main procedure*: Sqrt  
*Input*: real value X  
*Output*: the square root of X

### erfriemann

*Main procedure*: erfRiemann  
*Input*: real value X and integer n  
*Output*: a Riemann sum over n segments, approximating the value of the Gaussian error function for X

## How to write SPARK programs that can be verified using PolyPaver

TODO: 
* List replacements for Ada FP operations and functions.  
* State that in annotations, numerical operations retain their exact meaning.
* List annotation functions understood by polypaver (such as such as polypaver.exact.sqrt). 

To generate correctness theorems for a program PolyPaver uses the SPARK Examiner VC generator to produce a set of VCs. As the currently available version of the Examiner treats flaoting point operations as exact real arithmetic, it is necessary to short-circuit the VC generation process. To thi end, PolyPaver provides a SPARK Ada package with an interface to the Ada numerics packages and with a number of abstract operations (so-called proof functions) that may be used in annotations to encode accuracy properties of SPARK flaoting point programs. The SPARK tools also treat numeric expressions in annotations as exact real expressions and therefore abstract versions of the standard numeric operations are not needed. PolyPaver does however provide a number of extensions to the SPARK annotation language, such as an interval constrctor, integral operrator and interval containment relation, to make it convenient to express a accuracy constraints involving special fucntions.

## Generation of verification conditions (VCs):

In the program main folder, execute:

    > spark @peak
    > sparksimp

{'fraction_non_alphanumeric': 0.05247417074497009, 'fraction_numerical': 0.004893964110929853, 'mean_word_length': 4.712732919254658, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '888225', 'n_tokens_mistral': 981, 'n_tokens_neox': 885, 'n_words': 516}