# Algorithmic logic: Różnice pomiędzy wersjami

Skocz do: nawigacji, wyszukiwania

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
$\mathrm{Nic} \vdash \forall_{n_0 \in Node} \forall_{k \in Key}\,[\textbf{call } insert(n_0,k)]contains(n_0,k)$
i.e. it is a logical consequence of admitting declarations of class Node and functions insert and contains, that for every object $n_0$, and for every element $k$ of type $Key$, after execution of command $insert(n_),k)$ holds $contains(n_0,k)$.
The listing of Nic follows:

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;
}