Algorithmic logic: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
Linia 9: Linia 9:
 
-----------------
 
-----------------
 
  class Node
 
  class Node
{
+
{
 
   Node l,r;
 
   Node l,r;
 
   Key k;
 
   Key k;
 
 
   Node( Key _k ) : k(_k) {}
 
   Node( Key _k ) : k(_k) {}
}
+
}
 
+
void insert( Node n, Key k )
+
void insert( Node n, Key k )
{
+
{
 
   loop
 
   loop
 
   {
 
   {
Linia 40: Linia 39:
 
       return;
 
       return;
 
   }
 
   }
}
+
}
 
+
bool contains( Node n, Key k )
+
bool contains( Node n, Key k )
{
+
{
 
   while( n )
 
   while( n )
 
   {
 
   {
Linia 55: Linia 54:
 
   }
 
   }
 
   return false;
 
   return false;
}
+
}
 +
-----------------

Wersja z 21:43, 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] 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;
}