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_{...")
 
m
 
(Nie pokazano 8 pośrednich wersji utworzonych przez tego samego użytkownika)
Linia 1: Linia 1:
Are you ready?
+
Algorithmic logic is a logical calculus. More than this it is also a ''calculus of programs''.
'''A challenge'''<br />
+
We begin with an example ot its usefulness.
Given the following piece of software prove or disprove the following formula<br />
+
Are you ready?<br />
<math> \vdash \forall_{n_0 \in Node} \forall_{e \in T}\,[\textbf{call } insert(n_0,e)]contains(n_0,e)  </math>
+
 
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)$.
+
'''A challenge''' (presented by Pawel Susicki) <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 />
 +
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:
 +
-----------------
 +
<small>
 +
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;
 +
}
 +
</small>
 +
-----------------
 +
A piece of cake? Not so easy. Your answer should be written in the format close to a formal proof. It means, it should be easy to verify the correctness of your proof in an  automated way. Therefore, the proof should be a sequence of steps. You are not allowed to explain how the program is executed, no hands waving. Instead you are limited to use these declarations and  some inference rules and axioms.

Aktualna wersja na dzień 20:19, 16 paź 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. Your answer should be written in the format close to a formal proof. It means, it should be easy to verify the correctness of your proof in an automated way. Therefore, the proof should be a sequence of steps. You are not allowed to explain how the program is executed, no hands waving. Instead you are limited to use these declarations and some inference rules and axioms.