Utilize este link para identificar ou citar este item:
https://bdm.unb.br/handle/10483/18357
| Título: | Mechanization and overhaul of feature featherweight Java |
| Autor(es): | Abreu Júnior, Pedro da Costa |
| Orientador(es): | Almeida, Rodrigo Bonifácio de |
| Assunto: | Software
Linhas de Produtos de Software (LPS)
Java (Linguagem de programação de computador) |
| Data de apresentação: | 8-Ago-2017 |
| Data de publicação: | 21-Nov-2017 |
| Referência: | ABREU JÚNIOR, Pedro da Costa. Mechanization and overhaul of feature featherweight Java. 2017. viii, 25 f., il. Trabalho de Conclusão de Curso (Bacharelado em Ciência da Computação)—Universidade de Brasília, Brasília, 2017. |
| Abstract: | Specifying a language using an Interactive Theorem Prover (ITP) is seldom faithful to its original pen-and-paper specication. However, the process of mechanizing a language and type safety proofs might also unearth insights for improving the original specication. In this work, we detail some design decisions related to our process of first specifying Featherweight Java (FJ) in Coq and thus evolving such a specication to prove the type system properties of an revised version of Feature Featherweight Java (FFJ)-a core-calculus for a family of languages that address variability management in highly congurable systems, such as software product lines (SPLs); which we name as Overhaul Feature Featherweight Java (FFJ*). Indeed, FFJ* is the first mechanization of FFJ, and as such it might also help researchers to derive proofs about software product line renements without considering several assumptions about the underlying SPL assets. We believe that the whole process led us to a clearer, unambiguous, and equivalent syntax and semantics of FFJ, while keeping the proofs as well as our FJ extensions as simple as possible. |
| Informações adicionais: | Trabalho de conclusão de curso (graduação)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2017. |
| Aparece na Coleção: | Ciência da Computação
|
Este item está licenciado na Licença Creative Commons
