Algorithmic logic: Różnice pomiędzy wersjami
(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 | + | 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 /> |
− | + | 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;
}