Algorithmic logic: Różnice pomiędzy wersjami
Z Lem
| Linia 5: | Linia 5: | ||
'''A challenge'''<br /> | '''A challenge'''<br /> | ||
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<br /> | 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<br /> | ||
| − | <math> \mathrm{Nic} \vdash \forall_{n_0 \in Node} \forall_{k \in Key}\,[\textbf{call } insert(n_0,k)]contains(n_0,k) </math><br /> | + | ::<math> \mathrm{Nic} \vdash \forall_{n_0 \in Node} \forall_{k \in Key}\,[\textbf{call } insert(n_0,k)]contains(n_0,k) </math><br /> |
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>k </math> of type <math>Key </math>, after execution of command <math>insert(n_),k) </math> holds <math>contains(n_0,k) </math>. <br /> | 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>k </math> of type <math>Key </math>, after execution of command <math>insert(n_),k) </math> holds <math>contains(n_0,k) </math>. <br /> | ||
The listing of Nic follows: | The listing of Nic follows: | ||
Wersja z 21:50, 7 sty 2015
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] \mathrm{Nic} \vdash \forall_{n_0 \in Node} \forall_{k \in Key}\,[\textbf{call } insert(n_0,k)]contains(n_0,k) [/math]
- [math] \mathrm{Nic} \vdash \forall_{n_0 \in Node} \forall_{k \in Key}\,[\textbf{call } insert(n_0,k)]contains(n_0,k) [/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]k [/math] of type [math]Key [/math], after execution of command [math]insert(n_),k) [/math] holds [math]contains(n_0,k) [/math].
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;
}
