Algorithmic logic

Z Lem
Wersja AndrzejSalwicki (dyskusja | edycje) z dnia 21:29, 7 sty 2015

(różn.) ← poprzednia wersja | przejdź do aktualnej wersji (różn.) | następna wersja → (różn.)
Skocz do: nawigacji, wyszukiwania

Are you ready? A challenge
Given the following piece of software prove or disprove the following formula
[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)$.