Software Requirements Specifications

$\newcommand{\N}{\mathbb N} \newcommand{\Z}{\mathbb Z} \newcommand{\Q}{\mathbb Q} \newcommand{\R}{\mathbb R} \newcommand{\lt}{<} \newcommand{\gt}{>} \newcommand{\amp}{&} \definecolor{fillinmathshade}{gray}{0.9} \newcommand{\fillinmath}[1]{\mathchoice{\colorbox{fillinmathshade}{$\displaystyle \phantom{\,#1\,}$}}{\colorbox{fillinmathshade}{$\textstyle \phantom{\,#1\,}$}}{\colorbox{fillinmathshade}{$\scriptstyle \phantom{\,#1\,}$}}{\colorbox{fillinmathshade}{$\scriptscriptstyle\phantom{\,#1\,}$}}} $

Subsection 6.2.6 Software Requirements Specifications

Suppose that I need someone (possibly even myself) to write a program to solve some problem that I have in mind. I need a formal way to describe what the program is supposed to do. The logical framework that we’ve just developed can help me.

In particular, we can write logical statements that describe three things:

Anything that can be assumed to be true when the program begins. We’ll call that the program’s precondition (since “pre” means “before”).
Everything that we want to guarantee must be true when the program ends. We’ll call that the program’s postcondition (since “post” means “after”).
Key properties that must be maintained as the program executes. We’ll call these invariants. (They don’t change even as other things are changing as the program makes progress toward its goal).