Algorithmic logic - Historia wersji

AndrzejSalwicki o 19:19, 16 paź 2015

2015-10-16T19:19:57Z

AndrzejSalwicki o 21:19, 7 sty 2015

2015-01-07T21:19:17Z

AndrzejSalwicki o 21:09, 7 sty 2015

2015-01-07T21:09:11Z

AndrzejSalwicki o 21:05, 7 sty 2015

2015-01-07T21:05:23Z

AndrzejSalwicki o 20:59, 7 sty 2015

2015-01-07T20:59:48Z

AndrzejSalwicki o 20:50, 7 sty 2015

2015-01-07T20:50:12Z

AndrzejSalwicki o 20:48, 7 sty 2015

2015-01-07T20:48:57Z

AndrzejSalwicki o 20:43, 7 sty 2015

2015-01-07T20:43:39Z

AndrzejSalwicki o 20:41, 7 sty 2015

2015-01-07T20:41:20Z

AndrzejSalwicki: Utworzono nową stronę "Are you ready? '''A challenge'''
Given the following piece of software prove or disprove the following formula
$\vdash \forall_{n_0 \in Node} \forall_{..."$

2015-01-07T20:29:10Z

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_{..."

Nowa strona

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_{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)$.

@@ Linia 59: / Linia 59: @@
 </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 hsnds waving. Instead you are limited to use these declarations and  some inference rules and axioms.
+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.

@@ Linia 59: / Linia 59: @@
 </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 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.
+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 hsnds waving. Instead you are limited to use these declarations and  some inference rules and axioms.

@@ Linia 3: / Linia 3: @@
 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 />
 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>
 -----------------
-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.

← poprzednia wersja		Wersja z 21:05, 7 sty 2015
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.

@@ Linia 9: / Linia 9: @@
 The listing of Nic follows:
 -----------------
   class Node
+  {
@@ Linia 56: / Linia 57: @@
    return false;
+  }
 -----------------

← poprzednia wersja		Wersja z 20:43, 7 sty 2015
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;
−	}	+	}
		+	-----------------

@@ 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 />
-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>.