Autor(es): Abreu Júnior, Pedro da Costa
Data: 2017
Origem: Oasisbr
Assunto(s): Software; Linhas de Produtos de Software (LPS); Java (Linguagem de programação de computador); Software; Software; Linhas de Produtos de Software (LPS); Linhas de Produtos de Software (LPS); Java (Linguagem de programação de computador); Java (Linguagem de programação de computador)
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.
Submitted by Patricia Souza da Silva (patriciasilva@bce.unb.br) on 2017-09-11T18:57:00Z No. of bitstreams: 3 license_text: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) 2017_PedroAbreuJunior_tcc.pdf: 485744 bytes, checksum: d96226c2e009a8539942089c2553ffbe (MD5)
Approved for entry into archive by Luanna Maia (luanna@bce.unb.br) on 2017-11-21T13:51:28Z (GMT) No. of bitstreams: 3 license_text: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) 2017_PedroAbreuJunior_tcc.pdf: 485744 bytes, checksum: d96226c2e009a8539942089c2553ffbe (MD5)
Made available in DSpace on 2017-11-21T13:51:28Z (GMT). No. of bitstreams: 3 license_text: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) 2017_PedroAbreuJunior_tcc.pdf: 485744 bytes, checksum: d96226c2e009a8539942089c2553ffbe (MD5)
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.
