Algorithmic logic: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
(Utworzono nową stronę "Are you ready? '''A challenge'''<br /> Given the following piece of software prove or disprove the following formula<br /> <math> \vdash \forall_{n_0 \in Node} \forall_{...")
 
Linia 1: Linia 1:
Are you ready?
+
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?<br />
 +
 
 
'''A challenge'''<br />
 
'''A challenge'''<br />
Given the following piece of software 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> \vdash \forall_{n_0 \in Node} \forall_{e \in T}\,[\textbf{call } insert(n_0,e)]contains(n_0,e)  </math>
+
<math> NIC \vdash \forall_{n_0 \in Node} \forall_{e \in T}\,[\textbf{call } insert(n_0,e)]contains(n_0,e)  </math><br />
tzn, że jest logiczną konsekwencją przyjęcia definicji klasy $BST$ iż dla każdego węzła $n_0$ i każdego elementu $e$ typu $T$ po wykonaniu instrukcji $insert(n_),e)$ zachodzi $contains(n_0,e)$.
+
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;
 +
}

Wersja z 21:41, 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;

}