Algorithmic logic: Różnice pomiędzy wersjami

Z Lem
Skocz do: nawigacji, wyszukiwania
Linia 3: Linia 3:
 
Are you ready?<br />
 
Are you ready?<br />
  
'''A challenge'''<br />
+
'''A challenge''' (presented by Pawel Susicki) <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 <math> \mathrm{Nic}</math> 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 />
Linia 59: Linia 59:
 
</small>
 
</small>
 
-----------------
 
-----------------
A piece of cake? Not so easy. You are not allowed to explain how the program is executed. Instead you are limited to use these declarations and the inference rules of algoritmic logic (weel it axioms too) the result must be in a form close to a formal proof. For everybody will be able to verify if your proof is correct or not.
+
A piece of cake? Not so easy. You are not allowed to explain how the program is executed. Instead you are limited to use these declarations and the inference rules of algorithmic logic (well, its axioms too) the result must be in a form close to a formal proof. For everybody will be able to verify if your proof is correct or not.

Wersja z 22:09, 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 (presented by Pawel Susicki)
Given the piece of software [math] \mathrm{Nic}[/math] 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;
}


A piece of cake? Not so easy. You are not allowed to explain how the program is executed. Instead you are limited to use these declarations and the inference rules of algorithmic logic (well, its axioms too) the result must be in a form close to a formal proof. For everybody will be able to verify if your proof is correct or not.