Index

Symbols

--assumptions --ce-steps --check-counterexamples --checks-as-errors --counterexamples speeding up understanding counterexamples --cwe --function-sandboxing speeding up --info investigate unproved checks --level investigate unproved checks speeding up --limit-line calling an interactive prover command-line usage --limit-lines --limit-name --limit-region --limit-subp --memcached-server speeding up --memlimit --mode effect on output --no-global-generation --no-inlining forbid contextual analysis speeding up --no-loop-unrolling speeding up --output-header

--pedantic --proof proof strategies --proof-warnings --prover speeding up --replay sharing proofs speeding up --report example of use --steps max steps used speeding up --timeout speeding up --warnings warnings as error -A -D -f -gnata switch (compiler), [1] -gnateT -gnato -gnatp switch (compiler), [1] -j speeding up -k -U all files in project analyze all instances speeding up -u -W .spark files

A

Abstract_State access to subprogram access types access to object deallocation excluded feature ownership policy Address address-to-access-conversion aggregate aliasing absence of interference excluded feature Always_Terminates Annotate False_Positive for justifying check messages for subprogram termination Handler Inline_For_Proof Intentional Iterable; Iterable_For_Proof Iterable_For_Proof No_Bitwise_Operations No_Wrap_Around Prophecy Variable Skip_Proof; Skip_Flow_And_Proof

Aspect Aggregate Assert Assert_And_Cut Assertion_Error, [1] Assertion_Policy for precondition Assume justifying check messages assumptions Async_Readers state variables Async_Writers state variables Attach_Handler

B

Big_Numbers as alternative to overflow modes example of use bounded error Bronze level command-line switch data and control coupling early detection of errors GNAT Studio integration see also Depends see also Global tutorial

C

C language, [1] c-strings case-expression CENELEC EN 50128, [1], [2], [3] Check message (from GNATprove), [1] check messages categories of messages justification concurrency constant with variable inputs in state abstraction Constant_After_Elaboration and data races

Constraint_Error, [1] contextual analysis example of use Contract-based programming, [1] Contract_Cases and Old and Result example of use controlled types excluded feature counterexample GNAT Studio integration investigate unproved checks understanding counterexamples

D

data race deallocation declare-expression Default_Initial_Condition with value False Defensive code, [1] delta aggregate Depends automatic generation example of use in subprogram contract in task contract limitation

discriminant DO-178C / ED-12C, [1], [2], [3] Dynamic_Predicate

E

ECSS-Q-ST-80C, [1] Effective_Reads state variables Effective_Writes state variables EN 50128, [1], [2], [3] erroneous execution error messages exceptions Exceptional_Cases in precondition

executable contracts combining proof and test investigate unproved checks tutorial Exit_Cases expression function in refinement Extensions_Visible External and concurrency in state abstraction

F

False alarm, [1], [2], [3]

formal containers functional containers

G

generics analysis of instances excluded feature Ghost see ghost code ghost code investigate unproved checks manual proof manual proof using lemmas Ghost_Predicate Global automatic generation example of use for Bronze level, [1] in subprogram contract in task contract global variables in Depends contract in Global contract GNAT Studio integration analysis report Bronze level counterexample Gold level log file manual proof Silver level Stone level

GNATbench GNATmetric, [1] Gold level command-line switch correct component integration expression function functional correctness ghost code GNAT Studio integration investigate unproved checks see also Contract_Cases see also postcondition see also precondition tutorial writing contracts for functional correctness writing contracts for integrity goto excluded feature GPR_PROJECT_PATH at installation for SPARK library

I

IEC 60880, [1] IEC 61508, [1], [2], [3] IEC 62304, [1] if-expression imported subprograms writing contracts Info message (from GNATprove), [1] info messages suppression Initial_Condition initialization limitation

initialization (arrays) Initialized Initializes automatic generation inlining for proof example of use input-output Integration testing, [1] interrupt handler Invariant ISO 26262, [1]

L

lemma library example of use limitations Limitations of provers, [1] Liskov Substitution Principle loop and Loop_Entry automatic unrolling Loop_Entry Loop_Invariant automatic generation counting loops for Gold level, [1] for Silver level, [1] guidelines initialization loops mapping loops maximize loops rationale search loops tutorial update loops validation loops

Loop_Variant

M

main subprograms writing contracts manual proof GNAT Studio integration using Coq using ghost code using lemmas using the lemma library

migration from Ada project scenario migration from SPARK 2005 project scenario use of --no-global-generation

N

No_Caching

O

Object_Size Old Overflow_Mode

overlay ownership analysis of

P

Part_Of for concurrency in state abstraction Platinum level ghost code manual proof portability possible fix example of use Post see postcondition Post'Class how to use Postcondition, [1], [2], [3] postcondition and Old and Result example of use for subprogram pointer on dispatching operation pragma Assertion_Policy, [1]

Pre see precondition Pre'Class how to use Precondition, [1], [2], [3], [4], [5] precondition example of use, [1] for subprogram pointer on dispatching operation predicate Program_Exit project file and SPARK_Mode project attributes setting target and runtime setup Proof (as alternative to unit testing), [1] Proof mode (for GNATprove), [1] protected object and data races and deadlock

Q

Qualification (for GNATprove), [1]

quantified-expression over container

R

range Ravenscar recursion subprogram variant Refined_Depends Refined_Global

Refined_Post Refined_State Relaxed_Initialization initialization policy Result run-time error Runtime

S

side effects excluded feature in functions Side_Effects Silver level absence of run-time errors command-line switch GNAT Studio integration investigate unproved checks optimize run-time checks tutorial writing contracts for integrity Size SPARK Library SPARK_Mode, [1] rules usage speeding up --counterexamples --function-sandboxing --level --no-inlining --no-loop-unrolling --prover --replay --steps --timeout -j explicit package contracts

state abstraction and concurrency in package contract in subprogram contract Static_Predicate Stone level command-line switch GNAT Studio integration safe coding standard tutorial strings Subprogram_Variant Suspension_Object and data races Synchronous_State

T

Target tasking termination Always_Terminates excluded feature loop variant proving termination subprogram variant

tool interaction possible fix prove line or subprogram traversal function Type predicate, [1] Type_Invariant

U

Unchecked_Conversion Unchecked_Deallocation

Unevaluated_Use_Of_Old Unit testing, [1]

V

Valid limitation validity limitation

Visual Studio Code volatile state types variables

W

Warnings warnings (pragma) generated by proof suppression

workflows