Algorithmic logic: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
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]

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