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.
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! :-)