Guidelines for Safe and Secure Ada/SPARK
This document provides a reasonable set of coding standards to be applied to Ada/SPARK source code. The contents can be used as-is, or customized for a particular project.
This document was originally written by Patrick Rogers, and modified by Michael Frank.
- Introduction
- Definitions
- Dynamic Storage Management
- Safe Reclamation
- Concurrency
- Robust Programming Practice
- No Use of "others" in Case Constructs (RPP01)
- No Enumeration Ranges in Case Constructs (RPP02)
- Limited Use of "others" In Aggregates (RPP03)
- No Unassigned Mode-Out Procedure Parameters (RPP04)
- No Use of "others" in Exception Handlers (RPP05)
- Avoid Function Side-Effects (RPP06)
- Functions Only Have Mode "in" (RPP07)
- Limit Parameter Aliasing (RPP08)
- Use Precondition and Postcondition Contracts (RPP09)
- Do Not Re-Verify Preconditions In Subprogram Bodies (RPP10)
- Always Use the Result of Function Calls (RPP11)
- No Recursion (RPP12)
- No Reuse of Standard Typemarks (RPP13)
- Use Symbolic Constants For Literal Values (RPP14)
- Exception Usage
- Object-Oriented Programming
- No Class-wide Constructs Policy (OOP01)
- Static Dispatching Only Policy (OOP02)
- Limit Inheritance Hierarchy Depth (OOP03)
- Limit Statically-Dispatched Calls To Primitive Operations (OOP04)
- Use Explicit Overriding Annotations (OOP05)
- Use Class-wide Pre/Post Contracts (OOP06)
- Ensure Local Type Consistency (OOP07)
- Software Engineering
- References