Általános | Önéletrajz | Publikációk | Tárgyak | In English

Oktatott tárgyak

2008/2009 tavaszi félév

Formális szemantika

Szintézis és verifikáció

Komponens alapú szoftverfejlesztés

Archív

Programozási módszertan elmélete

Formális szemantika szeminárium

Formális szemantika 1.

Konkurens programozás Pascal-FC nyelven

Temporális logikák alkalmazásai

Letölthető anyagok

---

A TÁRGY NEVE: Formális szemantika
Célja: A programozási nyelvek szemantikájának formalizálása. A szemantikai leírások csoportosítása a felhasználói körök szerint. Az egyes alkalmazási területek bemutatása példákon keresztül.
Tartalmi ismeretek: A szemantikai leírások osztályozása: átmenet a szintaxistól a szemantikához, valódi szemantika definíciók. Fordítás attribútum-nyelvtanok alapján. Kétszintű nyelvtanok. Denotációs vagy matematikai szemantikák elméleti háttere és alkalmazásaik. Operációs vagy műveleti szemantikák és alkalmazásaik. A szemantikai leírások összehasonlítása.
Kialakítandó készségek: A programozási nyelvek szemantikai leírásának megértése. Készség szintű használata a különböző alkalmazási területeken. A programozási nyelvek elméleti hátterének mélyebb megértése.
Összes óraszám[1]: 60
A tantárgy kredit értéke[2]: 2
tanítási-tanulási órák típusa		előadás		laboratóriumi gyakorlat		tantermi gyakorlat	önálló tanulás
félévi óraszám		30					30
a számonkérés módja		kollokvium
heti óraszám
előzmény tárgyak	név		összes óraszám		rövid tartalom
Irodalom: H. R. Nielson, and F. Nielson: Semantics with Applications. A Formal Introduction. John Wiley &Sons Ltd., 1992. McIver, A., Morgan, C.: Programming Methodology. Springer-Verlag, 2003.
Ajánlott irodalom: Pagan, F. G. : Formal Specification of Programming Languages: A Panoramic Primer. Prentice Hall, INC. , 1981. Gordon, M. J. C.: The Denotational Description of Programming Languages. Springer-Verlag, 1979.

A TÁRGY NEVE: Szintézis és verifikáció
Célja: Programok helyességét bizonyító és helyes programokat előállítását szolgáló módszerek megismertetése és alkalmazása szekvenciális és párhuzamos programozási környezetben.
Tartalmi ismeretek: A helyes szekvenciális program fogalma. Szekvenciális helyességbizonyítási módszerek. Párhuzamos és konkurens program fogalma. Párhuzamos programok vizsgálata viselkedéselemzéssel. Párhuzamos programok helyességbizonyítási módszerei. Konkurens programok szintézis módszerei. Kontraktusok szerepe a helyességbizonyításban. Ágens alapú rendszerek és kontraktusok.
Kialakítandó készségek: Programok helyességének bizonyítására és helyes programok származtatására vonatkozó módszerek készség szintű elsajátítása szekvenciális és párhuzamos programozási környezetben. Az absztrakciós készség fejlesztése a helyes programrendszerek létrehozásában.
Összes óraszám[3]: 60
A tantárgy kredit értéke[4]: 2
tanítási-tanulási órák típusa		előadás		laboratóriumi gyakorlat		tantermi gyakorlat	önálló tanulás
félévi óraszám		30					30
a számonkérés módja		kollokvium
heti óraszám		2
előzmény tárgyak	név		összes óraszám		rövid tartalom
Irodalom: Kozma L., Varga L.: A szoftvertechnológia elméleti kérdései. ELTE Eötvös kiadó, 2006. Manna, Z.: Programozáselmélet. Műszaki könyvkiadó, 1981.
Ajánlott irodalom: Kröger, F.: Temporal Logic of Programs. Springer-Verlag, 1987. McIver, A., Morgan, C.: Programming Methodology. Springer-Verlag, 2003.

A TÁRGY NEVE: Komponens alapú szoftverfejlesztés
Célja: A komponens alapú szoftverfejlesztés alapfogalmainak, módszerének, eszközeinek bemutatása és az alkalmazás készségének kialakítása
Tartalmi ismeretek: A komponens alapú szoftverfejlesztés fogalma, összetevői. Komponens könyvtár, komponens modellek, szoftverarchitektúrák, egy konkrét programfejlesztési modell bemutatása. Egy eszköz megismerése verifikált rendszer létrehozására komponensekből. Komponensek verifikációja temporális logikai specifikáció esetén
Kialakítandó készségek: A komponens alapú szoftverfejlesztés elméleti problémáinak megértése és gyakorlati alkalmazása. Eszközök használata verifikált rendszerek létrehozására. Az absztrakciós készség növelése az alkalmazói rendszerek teljes életciklusában.
Összes óraszám[5]: 90
A tantárgy kredit értéke[6]: 3
tanítási-tanulási órák típusa		előadás		laboratóriumi gyakorlat		tantermi gyakorlat	önálló tanulás
félévi óraszám		30					60
a számonkérés módja		kollokvium
heti óraszám		2
előzmény tárgyak	név		összes óraszám		rövid tartalom
Irodalom: Bass, L., Clements P., Kazman R.: Software Architecture in Practice. Addison-Wesley, 2003. Clarke, E. M. Jr., Grumberg, O., Peled, D. A.: Model Checking. The MIT Press, 1999. Gross, H-G.: Component-based Software Testing with UML. Springer-Verlag, 2005.
Ajánlott irodalom: Kozma L., Varga L.: A szoftvertechnológia elméleti kérdései. ELTE Eötvös kiadó, 2006. Kröger, F.: Temporal Logic of Programs. Springer-Verlag, 1987. McIver, A., Morgan, C.: Programming Methodology. Springer-Verlag, 2005. Meyer, G. B.: Object-Oriented Software Construction, Second edition. Prentice Hall, 1997. Nyékyné Gaizler Judit eds.: Java 2 útikalauz programozóknak. ELTE TTK Hallgatói Alapítvány, 1999. Sike Sándor, Varga László: Szoftvertechnológia és UML. ELTE Eötvös kiadó, 2003.

Archív

Programozási módszertan elmélete

Szak:

Programtervező matematikus IV. évfolyam

Tantárgy félévigénye:

2 félév

Tantárgy heti óraszáma:

2 + 2

Eloadók:

Varga László professzor emeritus és
Kozma László habil. egy. docens

A tantárgy tematikája:

• Az objektum-orientált programozás legfontosabb fogalmai. Objektumok, adatelrejtés; absztrakció; öröklődés. Absztrakt adattípus egy matematikai modellje. Példák.
• Adattípusok fogalma. Algebrák és adattípusok. Példák.
• Az algebrai specifikáció alapfogalmai, szignatúramorfizmus, specifikációmorfizmus, az absztrakt adattípusok algebrai specifikációja.
• Az algebrai specifikáció elemzése. Tételek származtatása és bizonyítási módszerük.
• Absztrakt adattípusok megvalósítása. A reprezentáció fogalma és tétele, a helyes implementáció fogalma és tételei.
• Az adattípus egy komplex leírása: az osztály modell (típusosztály).
• A kétféle öröklés kifejezése az osztály modellben. Tételek.
• Az absztrakt adattípusok procedurális valamint elő- és utófeltételes specifikációja, az Alphard nyelv specifikációs eszközei.
• Kettős specifikáció: elő- és utófeltételes absztrakt, procedurális konkrét specifikáció, a megvalósítás helyessége.
• Kettős specifikáció: elő- és utófeltételes absztrakt, elő- és utófeltételes konkrét specifikáció, a megvalósítás helyessége. Az Alphard nyelv eszközei.
• Kettős specifikáció: algebrai absztrakt, elő- és utófeltételes konkrét specifikáció, a megvalósítás helyessége.
• A programhelyesség alapfogalmai. Floyd módszere programok teljes helyességének bizonyítására.
• Programok parciális helyességbizonyítása Hoare módszerével, a Hoare-módszer teljességi tétele.
• A teljes helyesség bizonyítása Hoare módszerével. Az iteráció helyességének tétele.
• A reprezentációs függvény rekurzív definíciója. A kettősvégű sorra vonatkozó eredmények.

Ajánlott irodalom:

[1]	Kozma László, Varga László: A szoftvertechnológia elméleti kérdései, ELTE Eötvös Kiadó, 2003
[2]	H. Ehrig and B. Mahr: Fundamentals of Algebraic Specification 1 Equations and Initaial Semantics, Springer-Vrlag Heidelberg, 1985.
[3]	H. Ehrig and B. Mahr: Fundamentals of Algebraic Specification 2 Module Specifications and Constraints, Springer-Vrlag Berlin Heidelberg, 1990.
[4]	R. Wieringa: A Survey of Structured and Object-Oriented Software Specification Methods and Techniques, ACM Computing Surveys, Vol. 30, No. 4, 1998, pp. 459-527.
[5]	A. Burns, G. Davies: Concurrent Programming, Addison-Wesley Pu. Co. Wokingham England 1993.
[6]	A. Trew and G. Wilson: Past, Present, Parallel, Springer-Verlag London Berlin Heidelberg, 1991.

Programozási módszertan elmélete I.

VIZSGATEMATIKA

2008. május

1. A szoftvertechnológia fogalma, programfejlesztési modellek. Az objektum elvű programozás legfontosabb fogalmai. Az absztrakt adattípus fogalma.

2. Absztrakt adattípus egy matematikai modellje. Példák. Az algebrák közötti homomorfizmus.

3. Absztrakt adattípusok és univerzális algebrák. Az algebrai specifikáció alapfogalmai, szignatúra morfizmus, specifikáció morfizmus.

4. Az adattípus osztályának specifikációja. Példák.

5. Az adattípus osztálya specifikációjának elemzése. Tételek származtatása és bizonyítási módszereik. Példák.

6. A kettős specifikációval kapcsolatos alapfogalmak. A reprezentációs függvény implicit és explicit definíciója. A kettős sorra vonatkozó eredmények.

7. Kettős specifikáció: algebrai absztrakt és algebrai konkrét specifikáció, a megvalósítás helyességére vonatkozó tételek.

8. Az absztrakt adattípusok elő- és utófeltételes valamint procedurális specifikációi. Kettős specifikáció: elő- és utófeltételes absztrakt, procedurális konkrét specifikáció, a megvalósítás helyessége.

9. Kettős specifikáció: elő- és utófeltételes absztrakt, elő- és utófeltételes konkrét specifikáció, a megvalósítás helyessége. Az Alphard nyelv eszközei.

10. Kettős specifikáció: algebrai absztrakt, elő- és utófeltételes konkrét specifikáció, a megvalósítás helyessége.

11. Szekvenciális programok helyességének fogalmai: valódi programok fogalma, a strukturált programok szintaxisa, a nem determinisztikus programok szintaxisa és szemantikája.

12. Valódi programok teljes helyességének bizonyítása Floyd módszerével.

13. Floyd módszerének formális definiciója.

14. Programok helyességbizonyítása Hoare módszerével. Az iteráció következtetési szabályának helyességére vonatkozó tétel.

15. A Hoare-módszer teljességi tétele.

16. Az adattípus egy komplex leírása: a kétféle öröklődés kifejezése az osztály modellben.

ugrás a lap tetejére

---

Formális szemantika szeminárium

Szak:

Programtervező matematikus

Tantárgy félévigénye:

1 félév

Tantárgy heti óraszáma:

2

A tantárgy tematikája:

A programozási nyelvek szemantikája területén elért legújabb eredmények áttekintése a szakirodalom alapján.

Ajánlott irodalom:

[1]	A témakör legújabb eredményeit tartalmazó szakirodalom.

ugrás a lap tetejére

---

Formális szemantika I.

Szak:

Programtervező matematikus

Tantárgy félévigénye:

1 félév

Tantárgy heti óraszáma:

2 óra előadás

Számonkérés módja:

kollokvium

A tantárgy tematikája:

• A szemantikai leírások fajtái. A denotációs szemantika matematikai alapjai.
• Szemantikus tartományok és szemantikus függvények.
• Fixpont-elmélet. A különböző nyelvi elemek jelentése.
• Az operációs szemantika alapjai.
• Átmenetrendszerek.
• A természetes és strukturális szemantikák lényege, tulajdonságai.
• A nem-determinisztikus és a párhuzamos utasítások jelentése.
• A különböző szemantikák összehasonlító elemzése.
• Az axiomatikus szemantika.
• Az attribútum-nyelvtanok és a kétszintű nyelvtanok mint a szemantikai leírás eszközei.
• Statikus programanalízis.
• Objektum elvű programozási nyelvek szemantikai problémái.

Ajánlott irodalom:

[1]	H. R. Nielson, F. Nielson: Semantics with Applications, A Formal Introduction, John Wiley & Sons, 1992.
[2]	F.G. Pagan: Formal Specification of Programming Languages: A Panoramic Primer, Prentice Hall, 1981
[3]	J. E. Stoy: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, 1977.
[4]	M. Abadi, L. Cardelli: A Theory of Objects, Springer-Verlag, 1996

ugrás a lap tetejére

---

Konkurens programozás Pascal-FC nyelven (speci)

Szak:

Az előadást bárki felveheti.

Tantárgy félévigénye:

1 félév

Tantárgy heti óraszáma:

2 óra előadás

A tantárgy tematikája:

• Hardver és szoftver architektúrák rövid áttekintése.
• A PASCAL-FC nyelv legfontosabb jellemzői.
• A Pascal-FC nyelvu programok fordítása, futtatása személyi számítógépen.
• A Pascal-FC nyelv párhuzamos utasításai:
• a párhuzamos végrehajtás utasítása;
• a folyamatok fogalma, nyelvi eszközei;
• a szinkronizációs utasítások;
• a kommunikációs utasítások;
• az üzenetváltás eszközei;
• az Ada-modell eszközei;
• monitorok, erőforrások stb.
• Programozás a különböző szoftver architektúrákban,
• (Linda-architektúra, processzfarmok stb.).
• Holtpont- és koplalásmentes rendszerek.
• Az egyes nyelvi elemek kifejezőerejének vizsgálata.
• Párhuzamos feladatok megoldása, a megoldások elemzése.

Ajánlott irodalom:

[1]	A. Burns, G. Davies: Concurrent Programming, Addison-Wesley Pu. Co. Wokingham England 1993.
[2]	A. Trew and G. Wilson: Past, Present, Parallel, Springer-Verlag London Berlin Heidelberg, 1991.
[3]	Kozma László, Varga László: A szoftvertechnológia elméleti kérdései, ELTE Eötvös Kiadó, 2003

ugrás a lap tetejére

---

Temporális logikák alkalmazásai

Szak:

Programtervező matematikus, doktoranduszok

Tantárgy félévigénye:

1 félév

Tantárgy heti óraszáma:

2 óra előadás

Számonkérés módja:

kollokvium

Előismeret:

A kurzusra azok a hallgatók iratkozhatnak be, akik a tudományegyetemek Logikai alapok a programozáshoz tantárgy anyagát eredményesen elsajátították. Ennek keretében megismerkedtek a klasszikus logika alapfogalmaival. Az ítéletkalkulus és a predikátum kalkulus nyelvével, következményfogalmával, a szintaktikus és szemantikus eldöntés problémákkal.

Oktatási célkitűzés:

A hallgatók az előadás keretében megismerkedhetnek a nem klasszikus logikák közül a temporális logikákkal, amelyek a modális logikáknak a programozás elmélete szempontjából nagyon fontos területét jelentik. Példákon keresztül mutatjuk be, hogy a temporális logikák segítségével a párhuzamos programok tulajdonságai jól leírhatók. A specifikációkból a helyes programok levezethetők.

Tematika:

• Az ítélet alapú lineáris idejű temporális logikák szintaxisa, szemantikája.
• A klasszikus ítéletkalkulus kiértékelési fogalmának kiterjesztése: a Temporális vagy Kripke-struktúra fogalma.
• A tautologikusan érvényes formula, az érvényesség, a kielégíthetőség fogalmai és a rájuk vonatkozó összefüggések, tételek.
• Az ítélet alapú temporális logika bizonyításelméleti tárgyalása.
• Az axiómarendszer helyessége, teljessége. Az elsőrendű temporális logika szintaxisa, szemantikája.
• A temporális logikák alkalmazásai konkurens programokra. Konkurens programok átmenet-gráfjai, multiprogramozott végrehajtásai.
• Programok invariancia és elevenségi tulajdonságai. Válaszadási képesség. Korrekt viselkedés; a kommunikációs protokoll tulajdonságai.
• Konkurens programok helyességbizonyításának egy kalkulusa.
• A tabló az ítéletalapú temporális logikákban. A tablón alapuló programszintézis lényege, példák.
• Az objektumok viselkedésének leírása múlt idejű operátorokkal kiterjesztett temporális logikákkal.
• Az intervallum logikák és alkalmazásaik.

Ajánlott irodalom:

[1]	F. Kröger: Temporal Logic of Programs, Springer-Verlag Berlin Heidelberg, 1987.
[2]	L. K. Dillon et. al.: A Graphical Interval Logic for Specifying Concurrent Systems, ACM Trans. On Soft. Eng. And Meth. 3 (2) 1994, pp. 131-165.
[3]	P.C. Attie, E. A. Emerson: Synthesis of Concurrent Programs with Many Similar Processes, ACM TOPLAS Vol. 20, No. 1, January 1998, pp. 51-115.
[4]	Hajdara, Sz. - Kozma, L. - Ugron, B.: Synthesis of a System Composed by Many Similar Objects, Annales Univ. Sci. Budapest., Sect. Comp., 22 (2003) pp.127-150

ugrás a lap tetejére

---

[1] Összes óraszám = félévi előadások +gyakorlatok+ laboratóriumi gyakorlatok száma +önálló tanulás becsült óraszáma

[2] A tantárgy kredit értékét célszerű az alábbi képlet kerekített értékével számolni:

kredit = összes óraszám/30

[3] Összes óraszám = félévi előadások +gyakorlatok+ laboratóriumi gyakorlatok száma +önálló tanulás becsült óraszáma

[4] A tantárgy kredit értékét célszerű az alábbi képlet kerekített értékével számolni:

kredit = összes óraszám/30

[5] Összes óraszám = félévi előadások +gyakorlatok+ laboratóriumi gyakorlatok száma +önálló tanulás becsült óraszáma

[6] A tantárgy kredit értékét célszerű az alábbi képlet kerekített értékével számolni:

kredit = összes óraszám/30