| Campo Dublin Core | Valor | Língua |
|---|
| dc.contributor.advisor | Almeida, Rodrigo Bonifácio de | - |
| dc.contributor.author | Abreu Júnior, Pedro da Costa | - |
| dc.identifier.citation | 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. | pt_BR |
| dc.description | 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. | pt_BR |
| dc.rights | Acesso Aberto | pt_BR |
| dc.subject.keyword | Software | pt_BR |
| dc.subject.keyword | Linhas de Produtos de Software (LPS) | pt_BR |
| dc.subject.keyword | Java (Linguagem de programação de computador) | pt_BR |
| dc.title | Mechanization and overhaul of feature featherweight Java | pt_BR |
| dc.type | Trabalho de Conclusão de Curso - Graduação - Bacharelado | pt_BR |
| dc.date.accessioned | 2017-11-21T13:51:28Z | - |
| dc.date.available | 2017-11-21T13:51:28Z | - |
| dc.date.submitted | 2017-08-08 | - |
| dc.identifier.uri | http://bdm.unb.br/handle/10483/18357 | - |
| dc.language.iso | Inglês | pt_BR |
| dc.description.abstract1 | 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. | pt_BR |
| Aparece na Coleção: | Ciência da Computação
|
