An Object-oriented Formal Notation: Executable Specifications in Clay = Una notación formal orientada a objetos : especificaciones ejecutables con Clay

Herranz Nieva, Ángel ORCID: https://orcid.org/0000-0002-6433-5681 (2010). An Object-oriented Formal Notation: Executable Specifications in Clay = Una notación formal orientada a objetos : especificaciones ejecutables con Clay. Thesis (Doctoral), Facultad de Informática (UPM). https://doi.org/10.20868/UPM.thesis.5682.

Description

Title: An Object-oriented Formal Notation: Executable Specifications in Clay = Una notación formal orientada a objetos : especificaciones ejecutables con Clay
Author/s:
Contributor/s:
Item Type: Thesis (Doctoral)
Read date: January 2010
Subjects:
Faculty: Facultad de Informática (UPM)
Department: Lenguajes y Sistemas Informáticos e Ingeniería del Software
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[thumbnail of ANGE_HERRANZ_NIEVA_2.pdf]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview

Abstract

This thesis presents Clay, a stateless object-oriented formal notation. Clay is class-based, has a nominal type system that integrates algebraic types and inheritance, has equality, method overriding with Scandinavian semantics, dynamic binding, and a rather permissive overloading.

The type system of Clay is used to reject illegal specifications, and also to help guide the translation schemes that define the Clay semantics and the generation of executable prototypes.

Clay has a first-order semantics that gives an interpretation in first-order logic of the main object-oriented constructions: inheritance, defining classes by cases, overloading, dynamic binding and static equality. Furthermore, the use of the concrete syntax of an automatic theorem prover (Prover9/Mace4) has allowed mechanising both, the Clay's meta-theory and specifications. For example, some of the theorems about Clay in this thesis have been proved semi-automatically.

The thesis presents also a compilation scheme of Clay specifications into Prolog programs. Code can be generated from implicit specifications, even recursive ones, something hard to find in other tools. My implementation takes advantage of various logic programming techniques in order to achieve reasonable efficiency: constraints, constructive negation, Lloyd-Topor transforms, incremental deepening search, etc.

A Clay compiler is also contributed, a tool that goes beyond the mathematical presentation of the translations into first-order logic and the synthesis of logic programs. I have built a compiler that supports syntax analysis of modular Clay specifications, type checking, translation of Clay specifications into first-order theories in Prover9/Mace4, and synthesis of executable Prolog prototypes.

More information

Item ID: 5682
DC Identifier: https://oa.upm.es/5682/
OAI Identifier: oai:oa.upm.es:5682
DOI: 10.20868/UPM.thesis.5682
Deposited by: Archivo Digital UPM
Deposited on: 07 Jan 2011 10:52
Last Modified: 10 Oct 2022 09:20
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM