Algorithmic logic

Algorithmic logic is a logical calculus. More than this it is also a calculus of programs. We begin with an example ot its usefulness. Are you ready?

A challenge
Given the piece of software NIC consisting of a class Node and two functions insert and contains (see below) prove or disprove the following formula
[math] NIC \vdash \forall_{n_0 \in Node} \forall_{e \in T}\,[\textbf{call } insert(n_0,e)]contains(n_0,e) [/math]
i.e. it is a logical consequence of admitting declarations of class Node and functions insert and contains, that for every object [math]n_0 [/math], and for every element [math]e [/math] of type [math]T [/math], after execution of command [math]insert(n_),e) [/math] holds [math]contains(n_0,e) [/math].

---

class Node

{

 Node l,r;
 Key k;

 Node( Key _k ) : k(_k) {}

}

void insert( Node n, Key k ) {

 loop
 {
   if( k < n.k )
     if( n.l )
       n := n.l;
     else
     {
       n.l := new Node( k );
       return;
     }
   else
   if( n.k < k )
     if( n.r )
       n := n.r;
     else
     {
       n.r := new Node( k );
       return;
     }
   else
     return;
 }

}

bool contains( Node n, Key k ) {

 while( n )
 {
   if( k < n.k )
     n := n.l;
   else
   if( n.k < k )
     n := n.r;
   else
     return true;
 }
 return false;

}