Some Methodological Remarks Inspired by the Paper ”On inner classes” by A. Igarashi and B. Pierce

• Autorzy: Langmaack H. , Salwicki A.
• Języki publikacji: EN

Abstrakty

EN

In [14] an axiomatic approach towards the semantics of FJI, Featherweight Java with Inner classes, essentially a subset of the Java-programming language, is presented. In this way the authors contribute to an ambitious project: to give an axiomatic definition of the semantics of programming language Java.1 At a first glance the approach of reducing Java’s semantics to that of FJI seems promising. We are going to show that several questions have been left unanswered. It turns out that the theory how to elaborate or bind types and thus to determine direct superclasses as proposed in [14] has different models. Therefore the suggestion that the formal system of [14] defines the (exactly one) semantics of Java is not justified. We present our contribution to the project showing that it must be attacked from another starting point. Quite frequently one encounters a set of inference rules and a claim that a semantics is defined by the rules. Such a claim should be proved. One should present arguments: 10 that the system has a model and hence it is a consistent system, and 20 that all models are isomorphic. Sometimes such a proposed system contains a rule with a premise which reads: there is no proof of something. One should notice that this is a metatheoretic property. It seems strange to accept a metatheorem as a premise, especially if such a system does not offer any other inference rules which would enable a proof of the premise. We are going to study the system in [14]. We shall show that it has many non-isomorphic models. We present a repair of Igarashi’s and Pierce’s calculus such that their ideas are preserved as close as possible.

Słowa kluczowe

EN

object-oriented programming; semantics; inheritance; inner classes; direct superclass; static semantics analysis; static binding; derivation calculus; model; minimal resp. least model

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2013
• Tom: Vol. 122, nr 3
• Strony: 227--274
• Opis fizyczny: Bibliogr. 35 poz., rys.

Twórcy

autor

Langmaack H.

• Institut für Informatik, Christian-Albrechts-Universität zu Kiel Christian-Albrechts-Platz 4, D-24098 Kiel, Germany

autor

Salwicki A.

• Faculty of Mathematics and Informatics, University Cardinal Stefan Wyszyński Wóycickiego 1-3, 01-938 Warszawa, Poland

Bibliografia

• [1] W. M. Bartol et al.. The Report on the Loglan’82 Programming Language. PWN, Warszawa, 1984
• [2] F.L.Bauer, H.Wössner. Algorithmic Language and Program Development. Springer, 1982
• [3] D.Bjoerner. Domain Engineering – Technology Management, Research and Engineering. COE Research Monograph Series, Vol. 4, JAIST Japan, 2009
• [4] R. Staerk, J. Schmid, E. Boerger. Java and the Java Virtual Machine- Definition, Verification, Validation, Springer-Verlag, June 2001
• [5] A.Church. The Calculi of Lambda-Conversion. Princeton University Press, 1941
• [6] O.-J.Dahl, K.Nygaard. Class and Subclass Declarations. In: J.N.Buxton (ed.). Simulation Programming Languages. Proc. IFIP Work. Conf. Oslo 1967, North Holland, Amsterdam, 158-174, 1968
• [7] E.W. Dijkstra. Recursive Programming. Numerische Mathematik 2, 312-318, 1960
• [8] G.Frege. Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle a.S., 1879
• [9] A.Grau, U.Hill, H.Langmaack. Translation of ALGOL60. Handbook for Automatic Computation, Vol. I, Part b (chief ed. K.Samelson), Springer 1967
• [10] J. Gosling, B. Joy, G. Steele. The Java Language Specification. First edition, Addison-Wesley 1996
• [11] J. Gosling, B. Joy, G. Steele, G. Bracha. The Java Language Specification. Second edition, Addison-Wesley 2000
• [12] J. Gosling, B. Joy, G. Steele, G. Bracha. The Java Language Specification. Third edition, Addison-Wesley 2005
• [13] J.D. Ichbiah. Ada Reference Manual. LNCS 106, Springer-Verlag, Berlin, Heidelberg, New York 1980
• [14] A. Igarashi, B. Pierce. On inner classes. Information and Computation 177, 56-89, 2002
• [15] P.Kandzia. On the “most recent”-property of ALGOL-like programs. In Proc. 2nd Coll. Automata Languages and Programming (J.Loeckx, ed.). LNCS 14, 97-111. Berlin, Heidelberg, New York, Springer 1974
• [16] A.Kreczmar, A.Salwicki, M.Warpechowski. Loglan’88 - Report on the Programming Language. LNCS 414, Springer, Berlin 1990
• [17] H.Langmaack. On Correct Procedure Parameter Transmission in Higher Programming Languages. Acta Informatica 2, 2, 110-142, 1973
• [18] H.Langmaack. Dijkstras fruchtbarer, folgenreicher Irrtum. Informatik Spektrum Band 33, Heft 3, 302-308, Heft 4, 384-392, Heft 6, 634-646, 2010
• [19] J. Loeckx, K. Sieber. The Foundation of Program Verification. Wiley-Teubner 1984
• [20] H.Langmaack, A. Salwicki, M.Warpechowski. On correctness and completeness of an algorithm determining inherited classes and on uniqueness of solutions. In: G.Lindemann et al., Proc. CS&P’2004, Caputh Sept. 24-26, Vol. 2, 319-329, Informatik-Berichte, Humboldt Univ. Berlin, 2004
• [21] H.Langmaack, A.Salwicki, M.Warpechowski. On a deterministic algorithm identifying direct superclasses in Java, Fundamenta Informaticae 85, 343-357, 2008
• [22] H.Langmaack, A.Salwicki, M.Warpechowski.Some methodological remarks inspired by the paper “On inner classes” by A.Igarashi and B.Pierce. Proc. CS&P’2008, Groß Vater See. Informatik-Berichte, Humboldt-Univ. Berlin, 448-462, 2008
• [23] H.Langmaack, A.Salwicki, M.Warpechowski. On an algorithm determining direct superclasses in Java-like languages with inner classes – its correctness, completeness and uniqueness of solutions. Information and Computation 207, 389-410, 2009
• [24] Z.Manna. Mathematical Theory of Computation. McGraw-Hill, 1974
• [25] J.McCarthy et al.. LISP 1.5 Programmer’s Manual. The M.I.T.Press, Cambridge, Mass., 1965
• [26] C.L.McGowan. The “most recent”-error: its causes and correction. In: Proc. ACM Conf. on Proving assertions about programs. SIGPLAN Notices 7, No.1, 191-202, 1972
• [27] O.L.Madsen, B.Moeller-Pedersen, K.Nygaard. Object Oriented Programming in the BETA Programming Language. Addison Wesley / ACM Presss, 1993, see also: Beta Programming Language, 2001, available from: http://www.daimi.au.dk/_beta/
• [28] G.Mirkowska, A.Salwicki, M. Srebrny, A. Tarlecki. First-order Specifications of Programmable Data Types, SIAM Journal on Computing, 30, pp. 2084-2096, 2001
• [29] Naur, P. (ed.) et al.: Report on the Algorithmic Language ALGOL60. Revised, Num. Math. 2, 106-136 (1960); Num. Math.4, 420-453, 1963
• [30] E.R.Olderog. Charakterisierung Hoarescher Systeme für ALGOL-ähnliche Programmiersprachen. Dissertation, Inst. F. Informatik u. Prakt. Math., Univ. Kiel, Bericht 5/81, 1981
• [31] G.L.Steele jr.. Common LISP - The Language. Digital Press 1984
• [32] H.Stoyan. Early LISP History (1956-1959). LFP’84 Proceedings of the 1984 ACM Symposium on LISP and Functional Programming, Austin, 5-8 August, 299-310. ACM 1984
• [33] W.M.Waite, G.Goos. Compiler Construction. Springer, New York Berlin Heidelberg Tokyo 1984
• [34] A.van Wijngaarden et al. (eds.). Report on the Algorithmic Language ALGOL68. Numerische Mathematik 14, 79-218, 1969
• [35] R.Wilhelm, D.Maurer. Űbersetzerbau - Theorie, Konstruktion, Generierung. Springer, Berlin Heidelberg New York 1992, 2. Aufl. 1997