JML- Based formal development of a Java card application for managing medical appointments

Although formal methods can dramatically increase the quality of software systems, they have not widely been adopted in software industry. Many software companies have the perception that formal methods are not cost-effective cause they are plenty of mathematical symbols that are difficult for non-experts to assimilate. The Java Modelling Language (short for JML) Section 3.3 is an academic initiative towards the development of a common formal specification language for Java programs, and the implementation of tools to check program correctness. This master thesis work shows how JML based formal methods can be used to formally develop a privacy sensitive Java application. This is a smart card application for managing medical appointments. The application is named HealthCard. We follow the software development strategy introduced by João Pestana, presented in Section 3.4. Our work influenced the development of this strategy by providing hands-on insight on challenges related to development of a privacy sensitive application in Java. Pestana’s strategy is based on a three-step evolution strategy of software specifications, from informal ones, through semiformal ones, to JML formal specifications. We further prove that this strategy can be automated by implementing a tool that generates JML formal specifications from a welldefined subset of informal software specifications. Hence, our work proves that JML-based formal methods techniques are cost-effective, and that they can be made popular in software industry. Although formal methods are not popular in many software development companies, we endeavour to integrate formal methods to general software practices. We hope our work can contribute to a better acceptance of mathematical based formalisms and tools used by software engineers. The structure of this document is as follows. In Section 2, we describe the preliminaries of this thesis work. We make an introduction to the application for managing medical applications we have implemented. We also describe the technologies used in the development of the application. This section further illustrates the Java Card Remote Method Invocation communication model used in the medical application for the client and server applications. Section 3 introduces software correctness, including the design by contract and the concept of contract in JML. Section 4 presents the design structure of the application. Section 5 shows the implementation of the HealthCard. Section 6 describes how the HealthCard is verified and validated using JML formal methods tools. Section 7 includes some metrics of the HealthCard implementation and specification. Section 8 presents a short example of how a client-side of a smart card application can be implemented while respecting formal specifications. Section 9 describes a prototype tools to generate JML formal specifications from informal specifications automatically. Section 10 describes some challenges and main ideas came acrorss during the development of the HealthCard. The full formal specification and implementation of the HealthCard smart card application presented in this document can be reached at https://sourceforge.net/projects/healthcard/.

A narratological analysis of D. M. Thoma`s: the white hotel (1981)

“A Narratological Analysis of D. M. Thomas’s The White Hotel (1981)” originated within a seminar on British Postmodernist Literature during the first Master’s Degree in “British and North-American Culture and Literature” (2001-04) at the Universidade da Madeira set up by the Department of English and German Studies. This dissertation seeks to present a narratological analysis of Thomas’s novel. The White Hotel stands as a paradigmatic example of the kind of literature that has dominated the British literary scene in the past three decades, commonly referred to as postmodernist fiction, owing to its formal craftsmanship (multiplicity of narrative voices and perspectives, mixing of differing genres and text types, inclusion of embedded narratives) alongside the handling of what are deemed as postmodernist topoi (the distinction between truth and lies, history and fantasy, fact and fiction, the questioning of the nature of aesthetic representation, the role the author and the reader hold in the narrative process, the instability of the linguistic sign, the notion of originality and the moral responsibility the author has towards his/her work), The narratological approach carried out in this research reveals that Thomas’s text constitutes an aesthetic endeavour to challenge the teleological drive that is inherent in any narrative, i. e., the inevitable progression towards a reassuring end. Hence, the subversion of narrative telling, which is a recurrent feature in Thomas’s remaining literary output, mirrors the contemporary distrust in totalising, hierarchised and allencompassing narratives. In its handling of historical events, namely of the Holocaust, The White Hotel invites us to reassess the most profound beliefs we were taught to take for granted: progress, reality and truth. In their place the novel proposes a more flexible conception of both the world and art, especially of literary fiction. In other terms, the world appears as a brutal chaotic place the subject is forced to adjust to. Accordingly, the literary work is deemed hybrid, fragmented and open. So as to put forth the above-mentioned issues, this research work is structured in three main chapters. The initial chapter – “What is Postmodernism?” – advances a scrutiny not only of the seminal but also of more recent studies on postmodernist literary criticism. Following this, in Chapter II – “Postmodernist British Fiction” – a brief overview of postmodernist British fiction is carried out, focusing on the fictional works that, in my opinion, are fundamental for the periodising of British postmodernism. In addition, I felt the need to include a section – “D. M. Thomas as a Postmodernist Novelist” – in which the author’s remaining literary output is briefly examined. Finally, Chapter III – “A Narratological Analysis of The White Hotel” – proposes a narratological analysis of the novel according to the particular Genettian analytical model. To conclude, my dissertation constitutes an approach to D. M. Thomas’s The White Hotel as a text whose very existence is substantiated in the foregrounding of the contingency of all discourses, meeting the postmodernist precepts of openness and subversion of any narrative that claims to be true, globalising and all-inclusive.