test.org

# -*- mode: org; coding: utf-8 -*-

#+TITLE:     Example Correctness Proofs
#+AUTHOR:    Marko Schütz-Schmuck
\include{extra-setup}

* linear search
  - sought: smallest index \(i\) with \(a_i = x\)
  - precondition: \(V \equiv n \in \naturals_0\)
  - postcondition:
    \begin{align*}
    P \equiv & n \in \naturals_0 \land k \in \naturals \land k \le n+1
    \land \textmath{found} \in \booleans \\
    & \land \forall 1 \le i < k.a_i \neq x \\
    & \land (k \le n \land a_k = x \land \textmath{found} \lor k = n+1 \land \neg \textmath{found})
    \end{align*}

** verify 						      :BMCOL:B_block:
   :PROPERTIES:
   :BEAMER_env: block
   :BEAMER_col: 0.44
   :END:

    \begin{minipage}{.9\linewidth}
    \(
    \begin{Condition}
    V
    \end{Condition}\)\endgraf
    \begin{Pseudocode}
    \STATE \(k \isassigned 1\)
    \WHILE{\(k \le n \land a_k \neq x\)} \STATE \(k \isassigned k+1\) \ENDWHILE
    \STATE \(\textmath{found} \isassigned k \le n\)
    \end{Pseudocode}
    \(
    \begin{Condition}
    P
    \end{Condition}\)
    \end{minipage}

** invariant						      :B_block:BMCOL:
   :PROPERTIES:
   :BEAMER_env: block
   :BEAMER_col: 0.52
   :END:
   \begin{align*}
   & n \in \naturals_0 \land k \in \naturals_0 \land k \le n+1 \\
   & \land \forall 1\le i<k. a_i
   \neq x
   \end{align*}

* proof overview
  #+BEGIN_LaTeX
  \(
  \begin{Condition}
  V
  \end{Condition}\)\endgraf
  \begin{Pseudocode}
  \STATE \(k \isassigned 1\)
  \WHILE{\(k \le n \land a_k \neq x\)} \STATE \(k \isassigned k+1\) \ENDWHILE
  \STATE \(\textmath{found} \isassigned k \le n\)
  \end{Pseudocode}
  \(
  \begin{Condition}
  P
  \end{Condition}\)
  #+END_LaTeX

#+LaTeX:  {\tiny
  \begin{prooftree}
  \AxiomC{\(V \implies I\substitute{1}{k}\)}
  \RightLabel{A2}
  \UnaryInfC{\hoareTriple{V}{\(S_i\)}{I}}
  \AxiomC{\(I \land B \implies I\substitute{k+1}{k}\)}
  \RightLabel{A2}
  \UnaryInfC{\hoareTriple{I \land B}{\(S_W\)}{I}}
  \AxiomC{\(I \land \neg B \implies P_1\)}
  \RightLabel{W2}
  \TrinaryInfC{\hoareTriple{V}{\(S_i\ \algorithmicseq\ W\)}{P_1}}
  \AxiomC{\hoareTriple{P\substitute{k\le n}{\textmath{found}}}{\(S_f\)}{P}}
  \RightLabel{A1}
  \UnaryInfC{\hoareTriple{P_1}{\(S_f\)}{P}}
  \RightLabel{S1}
  \BinaryInfC{\hoareTriple{V}{\(S_i\ \algorithmicseq\ W\ \algorithmicseq\ S_f\)}{P}}
  \end{prooftree}
#+LaTeX:  }

  termination: distance \(n+1 - k\)

* strengthen postcondition of loop body
  - rule (P1) allows strengthening postcondition
  - may make proving easier
* merge sorted sub-sequences
  - given: arrays \(a, b, c\) with \(a, b\) sorted by value
  - merge the sorted sequences of values into a sorted sequence of values in \(c\)
  - precondition:
    \begin{align*}
    V \equiv & n_a \in \naturals_0 \land \forall 1 \le i < n_a . a_i \le a_{i+1} \\
      \land & n_b \in \naturals_0\land \forall 1 \le i < n_b . b_i \le b_{i+1}
    \end{align*}
  - predicate for permutations: \([] \perm []\), \(a \& b \& c \perm d \& b \& e \iff a \&
    c \perm d \& e\) where \(\&\) has precedence over \(\perm\)
  - postcondition:
    \begin{align*}
    P \equiv & \appendop_{i=1}^{n_a+n_b} [c_{i}] \perm \appendop_{i=1}^{n_a} [a_i] \&
    \appendop_{i=1}^{n_b} [b_i]\\
    \land & \forall 1 \le i < n_a+n_b . c_i \le c_{i+1}
    \end{align*}
* proof obligations: black-box view
  1. \hoareTriple{V}{\(\textmath{merge}\)}{P}
  2. \(\textmath{merge}(d)\) is structurally like \(d\)
  3. \(\textmath{merge}\) will not modify any program variables other than \(c_i\) where
     \(1 \le i \le n_a+n_b\)
  4. \(\textmath{merge}\) terminates
* merge subprogram
  \begin{algorithmic}
  \DECLARE \((i_a, \naturals, 1), (i_b, \naturals, 1), (i_c, \naturals, 1)\)
  \WHILE{\(i_a \le n_a \lor i_b \le n_b\)}
  \IF{\(i_b > n_b \lor i_a \le n_a \land a_{i_a} \le b_{i_b}\)}
  \STATE \(c_{i_c} \isassigned a_{i_a}\)
  \STATE \(i_a \isassigned i_a + 1\)
  \ELSE
  \STATE \(c_{i_c} \isassigned b_{i_b}\)
  \STATE \(i_b \isassigned i_b + 1\)
  \ENDIF
  \STATE \(i_c \isassigned i_c +1\)
  \ENDWHILE
  \RELEASE \(i_a, i_b, i_c\)
  \end{algorithmic}

* proof obligations: looking under the hood
  1.

     \(
     \begin{Condition}
     V
     \end{Condition}\)
     \begin{Pseudocode}
     \DECLARE \((i_a, \naturals, 1), (i_b, \naturals, 1), (i_c, \naturals,
     1)\)
     \WHILE{\(i_a \le n_a \lor i_b \le n_b\)}
     \IF{\(i_b > n_b \lor i_a \le n_a \land a_{i_a} \le b_{i_b}\)}
     \STATE \(c_{i_c} \isassigned a_{i_a}\)
     \STATE \(i_a \isassigned i_a + 1\)
     \ELSE
     \STATE \(c_{i_c} \isassigned b_{i_b}\)
     \STATE \(i_b \isassigned i_b + 1\)
     \ENDIF
     \STATE \(i_c \isassigned i_c +1\)
     \ENDWHILE
     \RELEASE \(i_a, i_b, i_c\)
     \end{Pseudocode}
     \(
     \begin{Condition}
     P
     \end{Condition}\)

  2. maintains structure

  3. only modifies \(c_i\) where \(1 \le i \le n_a+n_b\)

* proving \hoareTriple{V}{\(\textmath{merge}\)}{P}
  - invariant: \(I \equiv \bigvee_{i=0}^8 I_i\) where
    - \(I_0 \equiv\) :: \(n_a \in \naturals_0 \land n_b \in \naturals_0\)
    - \(I_1 \equiv\) :: \(i_a \in \naturals_0 \land 1\le i_a\le n_a+1\)
    - \(I_2 \equiv\) :: \(i_b \in \naturals_0 \land 1\le i_b\le n_b+1\)
    - \(I_3 \equiv\) :: \(i_c-1 = i_a - 1 + i_b - 1\)
    - \(I_4 \equiv\) :: \(\appendop_{i=1}^{i_c-1} [c_{i}] \perm \appendop_{i=1}^{i_a-1} [a_i] \&
      \appendop_{i=1}^{i_b - 1} [b_i]\)
    - \(I_5 \equiv\) :: \((1 < i_c \land i_a \le n_a) \implies c_{i_c-1} \le a_{i_a}\)
    - \(I_6 \equiv\) :: \((1 < i_c \land i_b \le n_b) \implies c_{i_c-1} \le b_{i_b}\)
    - \(I_7 \equiv\) :: \(\forall 1 \le i < i_c-1 . c_i \le c_{i+1}\)
    - \(I_8 \equiv\) :: \(\forall 1 \le i < n_a . a_i \le a_{i+1} \land \forall 1
                        \le i < n_b . b_i \le b_{i+1}\)
  - symmetric wrt. renaming \(a \leftrightarrow b\)

* proof overview
#+LaTeX:  {\tiny
  \begin{prooftree}
  \AxiomC{\(V \implies I\substitute{1,1,1}{i_c,i_b,i_a}\)}
  \RightLabel{S1\(^+\), D1}
  \UnaryInfC{\hoareTriple{V}{\(\textmath{init}\)}{I}}
  \end{prooftree}
#+LaTeX: }
  - \(B_1 \land B_2 \iff i_a\le n_a \land (i_b > n_b \lor a_{i_a}\le b_{i_b})\) and \(B_1
    \land \neg B_2 \iff i_b\le n_b \land (i_a > n_a \lor b_{i_b} < a_{i_a})\)
#+LaTeX:  {\tiny
  \begin{prooftree}
  \AxiomC{\(\vdots\)}
  \UnaryInfC{\hoareTriple{I \land B_1 \land B_2}{\(S_1\)}{I\substitute{i_c+1}{i_c}}}
  \AxiomC{\(I \land i_b\le n_b \land (i_a > n_a \lor b_{i_b} \le a_{i_a}) \implies I\substitute{i_c+1,i_b+1,b_{i_b}}{i_c,i_b,c_{i_c}}\)}
  \RightLabel{S1, A1, A2}
  \UnaryInfC{\hoareTriple{I \land i_b\le n_b \land (i_a > n_a \lor b_{i_b} \le a_{i_a})}{\(S_1\)}{I\substitute{i_c+1}{i_c}}}
  \RightLabel{P1}
  \UnaryInfC{\hoareTriple{I \land i_b\le n_b \land (i_a > n_a \lor b_{i_b} < a_{i_a})}{\(S_1\)}{I\substitute{i_c+1}{i_c}}}
  \UnaryInfC{\hoareTriple{I \land B_1 \land \neg B_2}{\(S_2\)}{I\substitute{i_c+1}{i_c}}}
  \RightLabel{IF1}
  \BinaryInfC{\hoareTriple{I \land B_1}{\(S\)}{I\substitute{i_c+1}{i_c}}}
  \end{prooftree}
#+LaTeX: }
#+LaTeX: {\tiny
  \begin{prooftree}
  \AxiomC{\hoareTriple{V}{\(\textmath{init}\)}{I}}
  \AxiomC{\hoareTriple{I \land B_1}{\(S\)}{I\substitute{i_c+1}{i_c}}}
  \RightLabel{S1, A1}
  \UnaryInfC{\hoareTriple{I \land B_1}{\(S\ \algorithmicseq\ i_c \isassigned i_c + 1\)}{I}}
  \AxiomC{\(I \land \neg B_1 \implies P\)}
  \RightLabel{W2}
  \TrinaryInfC{\hoareTriple{V}{\(\textmath{init}\ \algorithmicseq\ W\)}{P}}
  \AxiomC{}
  \RightLabel{SP1}
  \UnaryInfC{\hoareTriple{P}{\(R\)}{P}}
  \RightLabel{S1}
  \BinaryInfC{\hoareTriple{V}{\(\textmath{init}\ \algorithmicseq\ W\ \algorithmicseq\ R\)}{P}}
  \end{prooftree}
#+LaTeX:  }


* Setup								   :noexport:
#+startup: beamer
#+EMAIL:     marko dot schutz at uprm dot edu
#+DESCRIPTION:
#+KEYWORDS:
#+LANGUAGE:  en
#+OPTIONS:   H:1 num:t toc:nil \n:nil @:t ::t |:t ^:t -:t f:t *:t <:t
#+OPTIONS:   TeX:t LaTeX:nil skip:nil d:nil todo:t pri:nil tags:not-in-toc
#+INFOJS_OPT: view:nil toc:nil ltoc:t mouse:underline buttons:0 path:http://orgmode.org/org-info.js
#+EXPORT_SELECT_TAGS: export
#+EXPORT_EXCLUDE_TAGS: noexport
#+LINK_UP:
#+LINK_HOME:
#+LaTeX_CLASS: beamer
#+LaTeX_HEADER:  \usepackage{colonequals}
#+LaTeX_HEADER:  \usepackage[noend]{algorithmic}
#+LaTeX_HEADER:  \usepackage{bussproofs}
#+LaTeX_HEADER:  \usepackage{nicefrac}
#+LaTeX_HEADER:  \institute{Department of Mathematical Sciences\\University of Puerto Rico at Mayagüez\\Mayagüez, PR}
#+BEAMER_FRAME_LEVEL: 1
#+COLUMNS: %40ITEM %10BEAMER_env(Env) %9BEAMER_envargs(Env Args) %4BEAMER_col(Col) %10BEAMER_extra(Extra)