Ugrás a tartalomhoz

Típusállapot-analízis

Ellenőrzött
A Wikipédiából, a szabad enciklopédiából

A típusállapot-analízis (protokollanalízis) a programelemzés egyik formája, amelyet a programozási nyelvekben (leggyakrabban objektumorientált) alkalmaznak. Típusállapotok használatával egy olyan műveletsorozatot határozunk meg, amelyeket egy adott típusú példányon végre lehet hajtani. A típusállapotok, amint a neve is mutatja, az állapotinformációkat az ilyen típusú változókhoz társítják. Ez az állapotinformáció arra szolgál, hogy fordításkor meghatározza, mely műveleteket lehet érvényesíteni egy adott példányra. Egy objektumon az általában futás közben végrehajtandó utasításokat, a típus állapotinformációin hajtják végre, módosítva azt, hogy kompatibilis legyen az objektum új állapotával.

A típusállapotok képesek viselkedési típusú finomítások reprezentálására, mint például: „Az 'A' metódust mindenképp 'B' előtt kell meghívni és a kettő között nem hívható meg 'C'!” A típusállapotok jól alkalmazhatók a nyílt/zárt szemantikát használó erőforrások ábrázolására olyan szemantikailag érvényes szekvenciák kikényszerítésével, mint a "nyitás, majd bezárás", szemben az érvénytelen szekvenciákkal, például egy fájl nyitott állapotban hagyásával. Az ilyen erőforrások magukban foglalják a fájlrendszer elemeit, a tranzakciókat, a kapcsolatokat és a protokollokat. Például a fejlesztők megadhatják, hogy a fájlokat vagy 'socketeket' meg kell nyitni, mielőtt elolvassák vagy írnák őket, és hogy azokat már nem lehet olvasni vagy írni a bezárásukat követően. A "typestate" név abból ered, hogy ez a fajta elemzés gyakran véges állapotgépként modellezi az egyes objektumtípusokat. Ebben az állapotgépben minden állapotnak van egy jól definiált megengedett módszere/üzenete, és a metódushívások állapotátmeneteket okozhatnak. A finomítási típusoknál alkalmazható lehetséges viselkedési modellként Petri-hálókat is javasoltak.[1]

A típusállapot-analízist Rob Strom mutatta be 1983-ban[2] az IBM Watson Lab-ban kifejlesztett Network Implementation Language (NIL) nyelven. Strom és Yemini formalizálta egy 1986-os cikkben[3] amely leírta, hogyan kell használni a típusállapotot a változók inicializálásának mértékének nyomon követésére, garantálva, hogy a műveleteket soha ne alkalmazzák a nem megfelelően inicializált adatokra, és tovább általánosították a Hermes programozási nyelvén.

Az elmúlt években különféle tanulmányok dolgozták ki a típusállapot-koncepció objektumorientált nyelvekre történő alkalmazásának módjait.[4] [5]

Megközelítés

[szerkesztés]
Astruct{int x;int y;int z;}.típusú változó inicializálásából származó nemlineáris típusállapotrács keletkezése

Strom és Yemini (1986) megkövetelte, hogy az adott típushoz tartozó típusállapotok részben rendezett halmaza úgy legyen megadva, hogy alacsonyabb rendű típusállapot kinyerhető legyen egy magasabból bizonyos információk elvetésével. Például a C nyelvben az int változó állapota: "nem inicializált" < "inicializált", és egy FILE* mutató állapota a "nem kiosztott" < "kiosztott, de nem inicializált" < "inicializált vannak, de a fájl nincs megnyitva" < "fájl megnyitva". Továbbá, Strom és Yemini megkövetelte, hogy mind a két típusnak legyen egy legnagyobb alsó határa, azaz a parciális sorrend még egy találkozó-félrács is valamint minden sorrendnek legyen adott egy legalacsonyabb eleme, mindig "⊥"-nek (alsó típus/base type) hívják.

Elemzésük azon egyszerűsítésen alapul, hogy minden v változóhoz csak egy típus van rendelve a program szövegének minden egyes pontjában; ha a p pontot két különböző végrehajtási útvonal éri el, és v az egyes utakon keresztül különböző típusokat örököl, akkor a v pontnál a p értéket a legmagasabb alsó határnak tekintjük. Például, a következő kódrészletben, az n változó az „inicializálva” és a „nem inicializált” állapotokat örökli az 'if', és az 'else' (üres) ágakban, illetve így a „nem inicializált” állapottal rendelkezik a feltételes utasítás lefutása után.

int n;        //itt 'n' állapota "nem inicializált"
if (...) {
  n = 5;      //'n' állapota "inicializált"
} else {
  /*ne csináljon semmit a kód*/  //'n' állapota "nem inicializált"
}           //a lefutás után 'n' állapota a legmagasabb alsó korlát, tehát "nem inicializált"

Minden alapműveletet[note 1] fel kell szerelni egy típusállapot-átmenettel, azaz minden paraméterhez meg kell adni a szükséges és biztosított típusállapotot a művelet előtt, illetve után. Például az fwrite(...,fd) metódusnál 'fd'-nek meg kell adnia a "fájl megnyitása" típusállapotot. Pontosabban, egy műveletnek több eredménye lehet, amelyek mindegyikének meg kell adnia a saját típusállapot-átmenetét. Például a C FILE *fd=fopen("foo","r" kód fd típusállapotát "fájl megnyitva" és "nem hozzárendelt" értékre állítja, ha a megnyitás sikeres, vagy sikertelen.

Minden két típusállapott 1 &lt;· t 2 után egyedi típusállapot kényszerítő műveletet kell rendelkezésre bocsátani, amelyek alkalmazása egy t 2 típusú objektumra az objektum állapotát t1-re csökkenti (bizonyos források felszabadításával). Például az fclose(fd) utasítás 'fd' típusállapotát a "fájl megnyitva" állapotból az "inicializált, de a fájl nincs megnyitva" állapotba kényszeríti.

Egy program végrehajtását típusállapot-korrekciónak nevezzük, ha:

  • minden egyes alapművelet előtt minden paraméter a típusállapot-átmenetéhez szükséges állapotban van
  • a program leállításakor az összes változó "⊥" típusban van.[note 2]

Egy programszöveget akkor nevezzük típusállapot-konzisztensnek, ha a megfelelő típusállapot-kényszer hozzáadásával átalakítható egy olyan programmá, amelynek pontjait statikusan meg lehet jelölni típusállapotokkal úgy, hogy a vezérlési folyamat által megengedett bármely út típusállapot-helyes legyen. Strom és Yemini olyan lineáris idejű algoritmust ad meg, amely ellenőrzi az adott programszöveg típusállapot-konzisztenciáját, és kiszámítja, hogy hova kell beilleszteni melyik kényszerítési műveletet, ha van ilyen.

Kihívások

[szerkesztés]

Pontos és hatékony típusállapot-elemzés elérése érdekében foglalkozni kell az álnevezés problémájával. Az álnevezés akkor fordul elő, ha egy objektumra több hivatkozás vagy mutató is rámutat. Ahhoz, hogy az elemzés helytálló legyen, az adott objektum állapotváltozásainak tükröződniük kell minden hivatkozásra, amely az adott objektumra mutat, de általában nehéz az összes ilyen hivatkozás nyomon követése. Ez különösen nehézzé válik, ha az elemzésnek modulárisnak kell lennie, vagyis egy nagy program minden részére külön-külön kell alkalmazni, a program többi részének figyelembe vétele nélkül.

Más kérdés, hogy egyes programok esetében a metódus, amely a legnagyobb alsó határt veszi fel a konvergáló végrehajtási utakon, és a megfelelő lefelé kényszerítési műveleteket hozzáadja, nem megfelelő. Például a következő programban a return 1[note 3] előtt a coord mindenx, y és z összetevőjét inicializáljuk, de Strom és Yemini megközelítése ezt nem ismeri fel, mivel a struktúra komponensek minden inicializálása a ciklus törzsén belül történik, ezért a ciklusba való újbóli belépéskor kényszeríteni kell, hogy megfeleljen a legelső cikluselem típusállapotának. Kapcsolódó probléma, hogy ez a példa megköveteli a típusállapot-átmenetek túlterhelését. Például a parse_int_attr("x",&coord->x) a "nincs komponens inicializálva" állapotot "x komponens inicializálva"-ra, de az "y komponens inicializálva" értéket "x és y komponens inicializálva"-ra változtatja.

int parse_coord(struct{int x;int y;int z;} *coord) {
  int seen = 0;   /*eltároljuk az attrubútumokat*/
  while (1)
    if   (parse_int_attr("x",&coord->x)) seen |= 1;
    else if (parse_int_attr("y",&coord->y)) seen |= 2;
    else if (parse_int_attr("z",&coord->z)) seen |= 4;
    else break;
  if (seen != 7)  /*amennyiben hiányzó attribútum van, a kód hibás*/
    return 0;
  ...        /*az összes attribútum jelenlétekor futtatandó kód*/
  return 1;
}

Típusállapot-következtetés

[szerkesztés]

Számos megközelítés törekszik arra, hogy típusállapotokat következtessen ki a programokból (vagy akár más tárgyakról, például szerződésekről). Közülük sokan a fordítási időben[6] [7] [8] [9] következtetnek a típusállapotokra, mások dinamikusan bányásszák a modelleket.[10] [11] [12] [13] [14] [15]

A típusállapotokat támogató nyelvek

[szerkesztés]

A típusállapot egy kísérleti koncepció, amely még nem lépett át a 'mainstream' programozási nyelvekre. Számos tudományos projekt azonban aktívan vizsgálja, hogyan lehet mindennapi programozási technikaként hasznosabbá tenni. Két példa a 'Plaid' és az 'Obsidian' nyelv, amelyeket Jonathan Aldrich csoportja fejleszt a Carnegie Mellon Egyetemen.[16] [17] További példák: a Clara[18] nyelvkutatási keretrendszer, a Rust nyelv korábbi verziói és a >> kulcsszó az ATS-ben.[19]

Megjegyzések

[szerkesztés]
  1. ↑ these include language constructs, e.g. += in C, and standard library routines, e.g.fopen()
  2. ↑ This aims at ensuring that e.g. all files have been closed, and all malloced memory has been freed. In most programming languages, a variable's lifetime may end before program termination; the notion of typestate-correctness has then to be sharpened accordingly.
  3. ↑ assuming that int parse_int_attr(const char *name,int *val) initializes *val whenever it succeeds

Hivatkozások

[szerkesztés]
  1. ↑ Jorge Luis Guevara D´ıaz: Typestate oriented design - A coloured petri net approach, 2010
  2. ↑ Strom, Robert E.. Mechanisms for compile-time enforcement of security, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL '83, 276–284. o.. DOI: 10.1145/567067.567093 (1983). ISBN 0897910907 
  3. ↑ Strom (1986). „Typestate: A programming language concept for enhancing software reliability”. IEEE Transactions on Software Engineering 12, 157–171. o, Kiadó: IEEE. DOI:10.1109/tse.1986.6312929. 
  4. ↑ DeLine (2004). „Typestates for Objects”. ECOOP 2004: Proceedings of the 18th European Conference on Object-Oriented Programming 3086, 465–490. o, Kiadó: Springer. DOI:10.1007/978-3-540-24851-4_21. 
  5. ↑ Bierhoff (2007). „Modular Typestate Checking of Aliased Objects”. OOPSLA '07: Proceedings of the 22nd ACM SIGPLAN Conference on Object-Oriented Programming: Systems, Languages and Applications 42 (10), 301–320. o. DOI:10.1145/1297027.1297050. 
  6. ↑ Guido de Caso, Victor Braberman, Diego Garbervetsky, and Sebastian Uchitel. 2013. Enabledness-based program abstractions for behavior validation. ACM Trans. Softw. Eng. Methodol. 22, 3, Article 25 (July 2013), 46 pages.
  7. ↑ R. Alur, P. Cerny, P. Madhusudan, and W. Nam. Synthesis of interface specifications for Java classes, 32nd ACM Symposium on Principles of Programming Languages, 2005
  8. ↑ Giannakopoulou, D., and Pasareanu, C.S., "Interface Generation and Compositional Verification in JavaPathfinder", FASE 2009.
  9. ↑ Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Permissive interfaces. Proceedings of the 13th Annual Symposium on Foundations of Software Engineering (FSE), ACM Press, 2005, pp. 31-40.
  10. ↑ Valentin Dallmeier, Christian Lindig, Andrzej Wasylkowski, and Andreas Zeller. 2006. Mining object behavior with ADABU. In Proceedings of the 2006 international workshop on Dynamic systems analysis (WODA '06). ACM, New York, NY, USA, 17-24
  11. ↑ Carlo Ghezzi, Andrea Mocci, and Mattia Monga. 2009. Synthesizing intensional behavior models by graph transformation. In Proceedings of the 31st International Conference on Software Engineering (ICSE '09). IEEE Computer Society, Washington, DC, USA, 430-440
  12. ↑ Mark Gabel and Zhendong Su. 2008. Symbolic mining of temporal specifications. In Proceedings of the 30th international conference on Software engineering (ICSE '08). ACM, New York, NY, USA, 51-60.
  13. ↑ Davide Lorenzoli, Leonardo Mariani, and Mauro Pezzè. 2008. Automatic generation of software behavioral models. In Proceedings of the 30th international conference on Software engineering (ICSE '08). ACM, New York, NY, USA, 501-510
  14. ↑ Ivan Beschastnikh, Yuriy Brun, Sigurd Schneider, Michael Sloan, and Michael D. Ernst. 2011. Leveraging existing instrumentation to automatically infer invariant-constrained models. In Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering (ESEC/FSE '11). ACM, New York, NY, USA, 267-277
  15. ↑ Pradel, M.; Gross, T.R., "Automatic Generation of Object Usage Specifications from Large Method Traces," Automated Software Engineering, 2009. ASE '09. 24th IEEE/ACM International Conference on, vol., no., pp.371,382, 16-20 Nov. 2009
  16. ↑ Aldrich: The Plaid Programming Language. (Hozzáférés: 2012. július 22.)
  17. ↑ Coblenz: The Obsidian Programming Language. (Hozzáférés: 2018. február 16.)
  18. ↑ Bodden: Clara. (Hozzáférés: 2012. július 23.)
  19. ↑ Xi: Introduction to Programming in ATS. (Hozzáférés: 2018. április 20.)

Fordítás

[szerkesztés]

Ez a szócikk részben vagy egészben a Typestate analysis 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.

Kapcsolódó szócikk

[szerkesztés]
A lap eredeti címe: „https://hu.wikipedia.org/w/index.php?title=Típusállapot-analízis&oldid=23797565”