Wyniki wyszukiwania - BazTech

1

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

Langmaack H., Salwicki A.

Fundamenta Informaticae

|

2013

|

Vol. 122, nr 3

227--274

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.

2

Verifying a Class: combining Testing and Proving

Mirkowska G., Salwicki A., Świda O.

Fundamenta Informaticae

|

2009

|

Vol. 95, nr 2/3

303-324

EN

The problem of correctness of a class C w.r.t. a specification S is discussed. A formal counterpart of the problem is the question well known in metamathematics, whether an algebraic structure is a model of a given theory. Now, this metamathematical problem has to be adapted to the context of software engineering. As a theory we consider the (algorithmic) specification S. The algebraic structure AC induced by the class C is our candidate for a model of S. Remark, that this problem differs from the correctness’ problem of an algorithm w.r.t. a pre- and a post-conditions. In the paper we consider the specification ATPQ of priority queues and the class PQS, and we verify the correctness of this class with respect to the specification ATPQ. Programmers and software companies prefer to test software instead of proving it. Surely, proving is more difficult, testing is easier. In this article we combine these two approaches. Hence, the following actions appear in our method of verification: experiment, observe, formulate hypotheses, prove. It is our hope that this method is of general use and adapts well to many practical cases of verification of object-oriented software.

3

Obliczenia rozproszone w sieci, możliwości Javy i oferta Loglanu

Salwicki A.

Telekomunikacja i Techniki Informacyjne

|

2008

|

nr 3-4

77-89

PL

Przedstawiono pewne narzędzia programowania rozproszonego. Mają one dwie istotne cechy: zwięzły, przejrzysty oraz jednolity mechanizm programowania do obliczeń rozproszonych i obliczeń współbieżnych, a także mechanizm w pełni obiektowy, wprowadzający protokół obcego wywołania metody procesu przez inny proces. Mechanizm ten został zrealizowany w języku programowania Loglan'82. Porównano to narzędzie z narzędziami oferowanymi przez Javę. Język programowania Java zawiera rozbudowany mechanizm programowania współbieżnego, którego podstawę stanowi predefiniowana klasa Thread (czyli wątek). Ponadto Javie towarzyszy odrębny mechanizm programowania rozproszonego, tzw. RMI. Jednak RMI nie jest częścią Javy.

EN

The paper presents certain tools of distributed programming, both sharing two important features: concise, transparent and unified programming mechanism for distributed and concurrent computing, and a fully objectoriented mechanism introducing a protocol for alien call of process method by another process. Such a mechanizm has been implemented in the Loglan'82 programming language. This tool has been compared to tools provided by Java. The Java programming language includes an extensive mechanism for concurrent programming, based on the pre-defined Thread. Additionally, Java is complemented by a separate distributed programming mechanizm known as RMI. Hovever, RMI is not a part of Java.

4

Algorithmic Logic + SpecVer = The Methodology for High Integrity Programming - Invited Paper

Mirkowska G., Salwicki A., Świda O.

Fundamenta Informaticae

|

2008

|

Vol. 85, nr 1-4

1-17

EN

Our aim is to present a methodology that integrates all phases of software's production beginning from the specification phase, through the phase of programming and finally the phase of verification of program against its specification. The theoretical background of the methodology is algorithmic logic [8]. The environment for practical activities of this software project is a plugin SpecVer [11] extending the Eclipse system.

5

A Deterministic Algorithm for Identifying Direct Superclasses in Java

Langmaack H., Salwicki A., Warpechowski M.

Fundamenta Informaticae

|

2008

|

Vol. 85, nr 1-4

343-357

EN

In an earlier article [5] we analyzed the problem of determining direct superclasses in Java and Java-like languages. We gave a specification of the problem showing that it closely reflects the requirements of [2]. We presented a non-deterministic algorithm and proved its correctness and completeness. This paper presents a deterministic algorithm which elaborates direct superclasses. The new algorithm is better for it presents all details of implementation and its cost seems lower than the cost of the non-deterministic algorithm. Another advantage of the proposed algorithm is error recovery. Should the algorithm report an error it continues its job and possibly reports more errors in one pass.

6

Andrzej Grzegorczyk's Contribution to Computer Science

Salwicki A.

Fundamenta Informaticae

|

2007

|

Vol. 81, nr 1-3

315-323

EN

The paper of Andrzej Grzegorczyk [19] on hierachy of the primitive recursive classes dates for 1953. This is the most frequently cited article of Polish author in computer science literature, having some hundreds citations. Moreover, many citations are in the papers of eminent computer scientists e.g. [10, 24, 33, 34, 31], sometimes the laureates of prestigious awards. In this paper we make an attempt to present Andrzej Grzegorczyk as a computer scientist.