000054606 001__ 54606
000054606 005__ 20190416220412.0
000054606 037__ $$aREP_WORK
000054606 245__ $$aFormal Development of Java Programs
000054606 269__ $$a1997
000054606 260__ $$c1997
000054606 336__ $$aReports
000054606 520__ $$aThe Java object-oriented programming language has been the subject of an important involvement from programmers and industry. Especially for applications related to the Web. The problem of such rapid penetration of Java programs into commercial product is that software engineers does not have any methodology and have to develop complex parallel applications. In this paper, we present, using a real (http://lglsun.epfl.ch/Team/GDM/DSGamma.html) but simple Web parallel application, a possible formal development methodology based on the stepwise refinement of CO-OPN/2 formal specifications. The application chosen is based on the Gamma paradigm, in which additions are realized across distributed multisets of integers maintained by local Java applets. CO-OPN/2 is an object-oriented specification formalism allowing the formal specification of abstract data types based on algebraic specification and of concurrent objects using a Petri net like approach. An interesting feature of CO-OPN/2 is that it gives a coherent solution for the expression of complex properties combining inheritance, concurrency and synchronizations. The refinement of formal descriptions for building progressively the Java program is presented in several refinement steps. This refinement process focuses on the distribution of data and treatments, and validation and verification are studied through the refinement of system properties.
000054606 700__ $$aDi Marzo Serugendo, Giovanna
000054606 700__ $$aGuelfi, Nicolas
000054606 8564_ $$s300157$$uhttps://infoscience.epfl.ch/record/54606/files/dimarzo-TR97-248.ps.gz$$zn/a
000054606 909C0 $$0252188$$pLGL
000054606 909CO $$ooai:infoscience.tind.io:54606$$preport$$qGLOBAL_SET
000054606 937__ $$aLGL-REPORT-1997-001
000054606 970__ $$aDimarzo:97:FDJP/LGL
000054606 973__ $$aEPFL$$sPUBLISHED
000054606 980__ $$aREPORT