Main | Curriculum Vitae | Publications
| Lectures | Membership
|
Lectures:
Spring Semester 2008/2009
Formal Semantics
Synthesis and Verification
Component-Based
Software Development
Theory of software methodology I-II
Semantics of
Programming Languages I.
Semantics of
Programming Languages - a special course
|
A TÁRGY NEVE:
Formal Semantics |
|||||||
|
Célja: Formal description of programming languages. Classification of semantic description methods
according to the application areas. |
|||||||
|
Tartalmi
ismeretek: Classification of
semantic descriptions. From syntax to semantics: attribute grammars,
two-level grammars. Formal methods:
denotational semantics, operational semantics. Equivalence results. |
|||||||
|
Kialakítandó
készségek: Understand of semantic
descriptions. Skills for applying different kind of semantics methods. Deep
understand of theoretical background of programming languages. |
|||||||
|
Ö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:
Synthesis and Verification |
|||||||
|
Célja: Correctness proof methods of sequential and parallel
programs. |
|||||||
|
Tartalmi
ismeretek: Basic notions of correct sequential
programs. Floyd method for proving partial end total correctness of
sequential flow charts programs. Hoare method for proving partial and total
correctness of structural programs. Basic notion of correct parallel and
concurrent programs. Behavioural
analysis of concurrent programs using shared variables, semaphores, monitors,
resources, remote procedure calls, message passing. Correctness proof methods
of parallel programs. Formal derivation of weakly and strongly correct
concurrent programs. A method for solving synchronization problems. Basic
notion of contracts. Contracts as a way of modeling a collection of agents. |
|||||||
|
Kialakítandó
készségek: Understand of theoretical
and practical aspects of correctness proof methods of programs. Understand of
formal methods for deriving weakly and strongly correct concurrent programs.
Developing skills for applying proof and synthesis methods. Ability to use
abstraction to create correct programs. |
|||||||
|
Ö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:
Component-Based Software Development |
|||||||
|
Célja: Basic notions of the component-based software
development. Methodologies, tools and their applications. |
|||||||
|
Tartalmi
ismeretek: Notion of component-based
software development. The notions of component library, component models and
software architectures. A component-based software development model. A tool
for developing correct system from prefabricated components. Temporal
logic-based verification techniques for components. |
|||||||
|
Kialakítandó
készségek: Understand of the
theoretical aspects of component-based software development process. Skills
for applying developing methods and tools for building system from verified
components. Increasing ability for using abstractions during whole life
cycles of programs. |
|||||||
|
Ö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 J. eds.: Java 2 útikalauz programozóknak. ELTE TTK
Hallgatói Alapítvány, 1999. Sike S., Varga L.: Szoftvertechnológia és UML. ELTE Eötvös kiadó, 2003. |
|||||||
Archives
Theory of software methodology I-II,
2+2
|
|
|
|
Description: |
|
|
Algebra
and abstract data types. Signatures, sigma-algebras, categories,
specification, signature-morphism, specification-morphism. Specification methods
for abstract data types, class specification. A specification methodology for
abstract data types: analysis of specification, analysis of representation
and implementation. Proof methods for program correctness. Correctness of
concurrent programs. A methodology for deriving correct concurrent programs.
Data types in concurrent environment, synchronisation interface.
Specification methods for synchronisation interface. Analysis of
specification, proof of consistence problems. |
|
Literatures:
|
[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. |
Semantics of
Programming Languages I., 2+0
|
|
|
|
Description: |
|
|
Semantic
description methods. Denotational semantics. Semantic domains and semantic
functions. Fixed point theory. The meaning of different language constructs.
Operational semantics. Transition systems. Natural semantics, structural
operational semantics. The meaning of non-deterministic and parallel
constructs. Equivalence results. Axiomatic program verification. Attribute
grammars and two-level grammars. Static program analysis. Semantic methods of
object-oriented languages. |
|
Literatures:
|
[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 |
Semantics of
Programming Languages - a special course, 0+2
|
|
|
|
Description: |
|
|
Overview
of new results on semantics of programming languages and on software
architectures. |
|
Literatures:
|
[1] |
Bass, L., Clements,
P., Kazmar, R.: Software Architecture in Practice (Second Edition),
Addison-Wesley, 2003. |
|
[2] |
Sparling, M.:
Lessons learned through six years of component-based development,
Communications of the ACM, pp. 47-53, Vol. 43., October 2000. |
|
[3] |
Fayad, M.E., Hamu,
D.S., Brugali, D.: Enterprise frameworks - Characteristics, criteria and
challenges, Communications of the ACM, pp. 39-46, Vol. 43., October 2000. |
|
[4] |
Kobryn, C.: Modeling
components and frameworks with UML, Communications of the ACM, pp. 31-38,
Vol. 43., October 2000. |