Applying Formal Methods to Programming

To my grandparents, Domenico, Giuseppe and Angela which are not here anymore, and Maria. ”In theory, there is no difference between theory and practice. But, in practice, there is.” — Jan L.A. van de Snepscheut T HIS THESIS concerns the design and evolution of two programming languages. The two contributions, unrelated with each other, are treated separately. The underlying theme of this work is the application of formal methods to the task of programming language design and implementation. Jeeg We introduce Jeeg, a dialect of Java based on a declarative replacement of the synchronization mechanisms of Java that results in a complete decoupling of the ‘business ’ and the ‘synchronization’ code of classes. Synchronization constraints in Jeeg are expressed in a linear temporal logic which allows to effectively limit the occurrence of the inheritance anomaly that commonly affect