SpecVer - Historia wersji

AndrzejSalwicki: /* Konstruowanie i analiza oprogramowania z pomocą logiki algorytmicznej. */

2020-03-16T11:16:51Z

‎Konstruowanie i analiza oprogramowania z pomocą logiki algorytmicznej.

AndrzejSalwicki o 10:28, 16 mar 2020

2020-03-16T10:28:30Z

AndrzejSalwicki: /* Bibliografia */

2018-10-02T13:04:56Z

‎Bibliografia

AndrzejSalwicki: /* Bibliografia */

2018-01-28T12:10:39Z

‎Bibliografia

AndrzejSalwicki: /* Konstruowanie i analiza oprogramowania z pomocą logiki algorytmicznej. */

2018-01-07T18:13:21Z

‎Konstruowanie i analiza oprogramowania z pomocą logiki algorytmicznej.

AndrzejSalwicki: /* Bibliografia */

2018-01-06T06:53:33Z

‎Bibliografia

AndrzejSalwicki: /* Bibliografia */

2018-01-06T06:47:30Z

‎Bibliografia

AndrzejSalwicki: /* Bibliografia */

2018-01-06T06:45:08Z

‎Bibliografia

AndrzejSalwicki: /* Konstruowanie i analiza oprogramowania z pomocą logiki algorytmicznej. */

2016-03-12T16:33:27Z

‎Konstruowanie i analiza oprogramowania z pomocą logiki algorytmicznej.

AndrzejSalwicki: /* Algorytmiczna teoria liczb naturalnych */

2016-03-06T21:36:34Z

‎Algorytmiczna teoria liczb naturalnych

@@ Linia 1: / Linia 1: @@
 == Konstruowanie i analiza oprogramowania z pomocą logiki algorytmicznej. ==
-Spróbuj swych sił -- czy potrafisz sformułowac teze o programie [[PawelG]] i podać dowód.
+'''Zagadka'''. Spróbuj swych sił -- czy potrafisz sformułowac tezę o programie [[PawelG]] i podać dowód.
 Proponujemy realizację projektu w którym będą współistnieć dokumenty co najmniej trzech typów:

← poprzednia wersja		Wersja z 10:28, 16 mar 2020
Linia 1:		Linia 1:
	== Konstruowanie i analiza oprogramowania z pomocą logiki algorytmicznej. ==		== Konstruowanie i analiza oprogramowania z pomocą logiki algorytmicznej. ==
		+
		+	Spróbuj swych sił -- czy potrafisz sformułowac teze o programie [[PawelG]] i podać dowód.

	Proponujemy realizację projektu w którym będą współistnieć dokumenty co najmniej trzech typów:		Proponujemy realizację projektu w którym będą współistnieć dokumenty co najmniej trzech typów:

@@ Linia 116: / Linia 116: @@
 # ({{odn|ref=nie|MSS|2008}}){{cytuj pismo|odn=tak|nazwisko=Mirkowska|imię=Grażyna|nazwisko2=Salwicki|imię2=Andrzej|nazwisko3=Świda|imię3=Oskar| tytuł=Verifying a Class: combining Testing and Proving|czasopismo=Fundamenta Informaticae|rok=2009|strony= |url=http://lem12.uksw.edu.pl/images/e/ef/Experimenting_Proving.pdf }}
 # ({{odn|ref=nie|MS|2015}}){{cytuj pismo|odn=tak|nazwisko=Mirkowska|imię=Grażyna|nazwisko2=Salwicki|imię2=Andrzej|  tytuł=Proving simulation class|czasopismo= |rok=2015 |strony= |url=http://lem12.uksw.edu.pl/images/4/41/ProvingSimulation.pdf  }}
-# ({{odn|ref=nie|MS|2015}}){{cytuj książkę|odn=tak|nazwisko=Mirkowska|imię=Grażyna|nazwisko2=Salwicki|imię2=Andrzej|  tytuł=Światły programista|czasopismo= |rok=2018 |strony= |url=  }}
+# ({{odn|ref=nie|MS|2018}}){{cytuj książkę|odn=tak|nazwisko=Mirkowska|imię=Grażyna|nazwisko2=Salwicki|imię2=Andrzej|  tytuł=Światły programista|czasopismo= |rok=2018 |strony= |url=  }}
 [[Category:SpecVer]]

@@ Linia 116: / Linia 116: @@
 # ({{odn|ref=nie|MSS|2008}}){{cytuj pismo|odn=tak|nazwisko=Mirkowska|imię=Grażyna|nazwisko2=Salwicki|imię2=Andrzej|nazwisko3=Świda|imię3=Oskar| tytuł=Verifying a Class: combining Testing and Proving|czasopismo=Fundamenta Informaticae|rok=2009|strony= |url=http://lem12.uksw.edu.pl/images/e/ef/Experimenting_Proving.pdf }}
 # ({{odn|ref=nie|MS|2015}}){{cytuj pismo|odn=tak|nazwisko=Mirkowska|imię=Grażyna|nazwisko2=Salwicki|imię2=Andrzej|  tytuł=Proving simulation class|czasopismo= |rok=2015 |strony= |url=http://lem12.uksw.edu.pl/images/4/41/ProvingSimulation.pdf  }}
-# ({{odn|ref=nie|MS|2015}}){{cytuj książkę|odn=tak|nazwisko=Mirkowska|imię=Grażyna|nazwisko2=Salwicki|imię2=Andrzej|  tytuł=Światły programista|czasopismo= |rok=2018 |strony= |url=http://lem12.uksw.edu.pl/images/f/fd/LoglanMan.pdf  }}
+# ({{odn|ref=nie|MS|2015}}){{cytuj książkę|odn=tak|nazwisko=Mirkowska|imię=Grażyna|nazwisko2=Salwicki|imię2=Andrzej|  tytuł=Światły programista|czasopismo= |rok=2018 |strony= |url=  }}
 [[Category:SpecVer]]

@@ Linia 20: / Linia 20: @@
 Materiały jakie tu zamieszczamy mają pokazać nasz sposób myślenia i kierunki poszukiwań.
-Kiedyś profesor Józef Winkowski<ref>wypowiedź ustna</ref> powiedział ''"stworzenie większego systemu programistycznego to praca podobna do zbudowania wielu teorii matematycznych"''. Dziś jesteśmy o tym przekonani. Dokładniej mam na myśli to, że nie wystarczy tworzyć moduły oprogramowania, ani interfejsy. Potrzebne sa specyfikacje. O specyfikacjach trzeba myśleć w ten sam sposób jak o aksjomatyzacjach teorii sformalizowanych i w związku z tym badać problemy niesprzeczności, pełności, kategoryczności. Co więcej podczas tworzenia werdyktów weryfikujących poprawność tworzymy teorie algorytmiczne i z twierdzeń tych teorii korzystamy podczas dalszej pracy nad kolejnymi programami.
+Kiedyś profesor Józef Winkowski<ref>wypowiedź ustna, ok. r. 1976</ref> niezobowiązująco powiedział ''"stworzenie większego systemu programistycznego to praca podobna do zbudowania wielu teorii matematycznych"''. Dziś potrafimy myśl tę precyzyjnie uzasadnic.. Dokładniej mamy na myśli to, że nie wystarczy tworzyć moduły oprogramowania, ani interfejsy. Potrzebne sa specyfikacje. O specyfikacjach trzeba myśleć w ten sam sposób jak o aksjomatyzacjach teorii sformalizowanych i w związku z tym badać problemy niesprzeczności, pełności, kategoryczności. Co więcej podczas tworzenia werdyktów weryfikujących poprawność tworzymy teorie algorytmiczne i z twierdzeń tych teorii korzystamy podczas dalszej pracy nad kolejnymi programami.
-Postaramy sie tę myśl zilustrowac kilkoma przykładami...
+Postaramy sie tę myśl zilustrować kilkoma przykładami...
 Propozycja:

@@ Linia 1: / Linia 1: @@
 == Konstruowanie i analiza oprogramowania z pomocą logiki algorytmicznej. ==
-Chcemy zaproponować realizację projektu w którym będą współistnieć dokumenty conajmniej trzech typów:
+Proponujemy realizację projektu w którym będą współistnieć dokumenty co najmniej trzech typów:
 * specyfikacje,
 * moduły klas, procedur, funkcji, etc.,
 * dokumenty zawierające argumenty rozstrzygające o poprawności  modułu względem specyfikacji.
-Projekt SpecVer jest niewątpliwie projektem trudnym. Ale sądzę, że mamy oryginalny pomysł.[[Analiza przykładu]]<br />
+Projekt SpecVer jest niewątpliwie projektem trudnym. Ale sądzę, że mamy oryginalny pomysł.Zobacz [[Analiza przykładu]]<br />
 Zanim przejdziemy do dalszych szczegółów:
 * będziemy rozwijać algorytmiczne teorie rozmaitych struktur i badać ich związki z odpowiednimi klasami,
-* jako test naszego podejścia proponujemy zbudowanie biblioteki klas podobnej do znanej bibioteki STL. Różnica ma polegać na tym, że w produkcie końcowym dla każdej klasy mają znaleźć się:
+* jako test naszego podejścia proponujemy zbudowanie biblioteki klas podobnej do znanej biblioteki STL. Różnica ma polegać na tym, że w produkcie końcowym dla każdej klasy mają znaleźć się:
 :* ''specyfikacja'' klasy <math>K</math> - lub inaczej mówiąc sygnatura i aksjomaty algorytmicznej teorii <math>T_K</math> opisujące nie tylko interfejs operacji, lecz także własności operacji na obiektach opisywanych przez klasę,
-:* ''implementacja'' czyli klasa <math>T_K</math>,
+:* ''implementacja'' czyli klasa <math>K</math>,
-:* ''weryfikacja'' czyli dowód tego, że klasa <math>T_K</math> zapewnia prawdziwość wszystkich własnośności wymienionych w aksjomatach teorii <math>T_K</math>
+:* ''weryfikacja'' czyli dowód tego, że klasa <math>K</math> zapewnia prawdziwość wszystkich własnośności wymienionych w aksjomatach teorii <math>T_K</math>

@@ Linia 66: / Linia 66: @@
 A2) <math>\forall x\, \neg x+1=0  </math><br />
 A3) <math>\forall x \forall y\, (x+1=y+1)\rightarrow{x=y}  </math><br />
-Z tych trzech aksjomatów potrafimy wyprowadzić wszystkie aksjomaty teorii Peano, w tym schemat indukcji.
+Z tych trzech aksjomatów potrafimy wyprowadzić wszystkie aksjomaty teorii Peano, w tym schemat indukcji.<br />
 Rozpatrzmy kilka przykładów:
 # algorytm Euklidesa - jak udowodnić poprawność tego algorytmu? Nie wynika ona z aksjomatów Peano.  Natomiast z algorytmicznego aksjomatu ''być liczbą naturalną'' wynika algorytmiczna formuła  <math>\forall x \{\textbf{while }\neg x=0 \textbf{ do }y:=y-1 \textbf{ od} \}(x=0) </math>.   Z tej algorytmicznej formuły -   wynika formuła algorytmiczna wyrażająca własnośc stopu algorytmu Euklidesa.