Finomítás (számítástechnika)

A finomítás a számítástechnika egy általános fogalma, amely különböző megközelítéseket ölel fel a helyes számítógépes programok előállítása és a meglévő programok egyszerűsítése érdekében, hogy lehetővé tegye azok hivatalos ellenőrzését.

Programfinomítás

Formális módszerekben a program finomítása az absztrakt (magas szintű) formális specifikáció igazolható átalakítása konkrét (alacsony szintű) futtatható programmá. A fokozatos finomítás lehetővé teszi ezen folyamat szakaszonkénti végrehajtását. Logikailag a finomítás általában magában foglalja az implikációt, de további komplikációk is lehetnek.

A termékhátrány (követelménylista) progresszív, időben történő előkészítését az agilis szoftverfejlesztési megközelítésekben, mint például a Scrum, általában finomításnak is nevezik.

Adatfinomítás

Az adatfinomítással egy absztrakt adatmodellt (például halmazok szempontjából) alakítanak át implementálható adatszerkezetekké (például tömbökké). A művelet finomítás egy rendszeren végrehajtott művelet specifikációját implementálható programmá (pl. eljárássá) alakítja. Az utófeltétel megerősíthető és/vagy az előfeltétel gyengíthető ebben a folyamatban. Ez a specifikáció valamely nemdeterminizmusát tipikusan egy teljesen determinisztikus implementációig csökkenti.

Például, x ∈ {1,2,3} (ahol x értéke a változónak egy művelet után) finomíthatjuk úgy, hogy x ∈ {1,2}, majd x ∈ {1}, és implementálni, mint X := 1. Az x: = 2 és x := 3 implementációi ebben az esetben ugyanúgy elfogadhatóak lennének, ha a finomításhoz más utat használunk. Vigyáznunk kell azonban arra, hogy ne pontosítsunk az x ∈ {} értékre (ami hamisnak felel meg), mivel ez kivitelezhetetlen; lehetetlen tagot kiválasztani az üres halmazból .

A reifikáció kifejezést is használják néha (feltalálója Cliff Jones). A visszahúzás egy alternatív technika arra az esetre, ha a hivatalos finomítás nem lehetséges. A finomítás ellentéte az absztrakció.

Finomítási kalkulus

A finomítási kalkulus egy (a Hoare-logika által inspirált) formális rendszer, amely elősegíti a program finomítást. A FermaT transzformációs rendszer a finomítás ipari erősségű megvalósítása. A B-Módszer egy olyan formális módszert is jelent, amely kiterjeszti a finomítási kalkulust egy komponensnyelvvel: ipari fejlesztésekben alkalmazták.

Finomítási típusok

A típuselméletben egy finomító típus egy predikátummal felruházott típus, amely feltételezhetően a finomított típusú elem bármelyikére vonatkozhat. A finomítási típusok előfeltételeket fejezhetnek ki ha függvény argumentumként használjuk őket, vagy utófeltételeket, ha visszatérési típusként: például egy olyan függvény típusa, amely természetes számokat fogad el és 5-nél nagyobb természetes számokat ad vissza így írható fel: $f:\mathbb {N} \rightarrow \{n:\mathbb {N} \,|\,n>5\}$ . A finomítási típusok tehát a viselkedésbeli altípushoz kapcsolódnak.

Források

1.  Cho, L (2009) "Adopting an Agile Culture A User Experience Team's Journey". Agile Conference: 416. doi:10.1109/AGILE.2009.76. ISBN 978-0-7695-3768-9.
2. Freeman, T.; Pfenning, F. (1991). "Refinement types for ML" (PDF). Proceedings of the ACM Conference on Programming Language Design and Implementation. pp. 268–277. doi:10.1145/113445.113468
3. Hayashi, S (1993). "Logic of refinement types". Proceedings of the Workshop on Types for Proofs and Programs. pp. 157–172. CiteSeerX 10.1.1.38.6346. doi:10.1007/3-540-58085-9_74.
4. Denney, E. (1998). "Refinement types for specification". Proceedings of the IFIP International Conference on Programming Concepts and Methods. 125. Chapman & Hall. pp. 148–166. CiteSeerX 10.1.1.22.4988

Fordítás

Ez a szócikk részben vagy egészben a Refinement (computing) című angol Wikipédia-szócikk ezen változatának fordításán alapul. Az eredeti cikk szerkesztőit annak laptörténete sorolja fel. Ez a jelzés csupán a megfogalmazás eredetét és a szerzői jogokat jelzi, nem szolgál a cikkben szereplő információk forrásmegjelöléseként.