Programozás visszavezetéssel

4 September 2008 (ELTE programming correctness) (4 comments)

Hát akkor nézzük, mivel is tervezek foglalkozni Fóthi Ákossal a hétfőn kezdődő félév során, progmatos nagyprogramom keretében.

Az alapötlet az, hogy gépi segítséggel bizonyítsunk programozási tételeket , visszavezetés segítségével, és az "ötleteket", az invenciózus lépéseket a felhasználó, ne pedig valamilyen hilbertiánus, féseggű MI-engine találja ki. Tehát a papírt-ceruzát váltanánk csak ki, a hibázás lehetőségét akarjuk csökkenteni és az eredmények menedzselhetőségét növelni.

A "Hello World" szintet például az jelenti majd, ha abból a tételből, hogy ismerjük tetszőleges f:ℤ→ℤ illetve β:ℤ→𝕃 függvények esetén az alábbi feladat (Hoare/Dijkstra/Fóthi értelemben) megoldását...

A: (m: ℤ) × (n: ℤ) × (l: 𝕃) × (i: ℤ) × (max: ℤ)
B: (m': ℤ) × (n': ℤ)
Q: m=m' ∧ n=n' ∧ m≤n ∧ [m, n]⊆dom(f)
R: Q ∧ l=(∃k∈[m,n]:β(k)) ∧ l⇒ (i∈[m,n] ∧ β(i) ∧ max=f(i) ∧ ∀k∈[m,n]:β(k)⇒f(k)≤max)

(egyrészt vegyük észre, hogy természetesen a feltételes maximumkeresésről van szó, másrészt gondolkodjunk el azon, milyen fun lehetett ezt egyenként, Unicode táblázatokat böngészve beírnom)

... be tudjuk látni, hogy akkor meg tudjuk oldani bármilyen, mondjuk g:ℤ→ℤ függvényre az egyszerű minimumkeresést is, vagyis az alábbi feladatot:

A: (m: ℤ) × (n: ℤ) × (i: ℤ) × (min: ℤ)
B: (m': ℤ) × (n': ℤ)
Q: m=m' ∧ n=n' ∧ m≤n ∧ [m, n]⊆dom(g)
R: Q ∧ i∈[m,n] ∧ min=g(i) ∧ ∀k∈[m,n]:g(k)≥min

Erre egyébként van már annyi szanaszét heverő Lisp kódrészletem, amennyiből valószínűleg össze lehetne kalapálni valamit, ami ennyit már épp majdnem tudna is. Stay tuned.


« Viki in a nutshell 
All entries
 Geekparty és egy breaking news »


Encsé 2008-09-05 00:10:35

Sajnos nálam a nagy X nem jelenik meg. Pedig pont nem én vagyok az, akinek fontokra lenne szüksége....

2a09 jobb lenne (n-ary multiplication) vagy 00d7 (multiplication)

A visszavezető rendszert meg nagyon várjuk.

cactus 2008-09-05 00:18:16

Így már jobb?

Cégünk mindig az Ön rendelkezésére áll, asszonyom.

Encsé 2008-09-05 22:43:24

sokkal

cooldavee 2008-09-06 23:38:00

Hülyék ezek? Egy női blogot sóztak ránk! :-)