Dissertação (mestrado)—Universidade de Brasília, Instituto de Letras, Departamento de Linguística, Português e Línguas Clássicas, Programa de Pós-Graduação em Linguística, 2018. / Submitted by Fabiana Santos (fabianacamargo@bce.unb.br) on 2018-08-22T19:17:25Z No. of bitstreams: 1 2018_RosaniKristineParaísoGarcia.pdf: 2789550 bytes, checksum: a0492b8e4403e5caca30e09c36a2fa26 (MD5) / Approved for entry into archive by Raquel Viana (raquelviana@bce.unb.br) on 2018-08-27T20:04:59Z (GMT) No. of bitstreams: 1 2018_RosaniKristineParaísoGarcia.pdf: 2789550 bytes, checksum: a0492b8e4403e5caca30e09c36a2fa26 (MD5) / Made available in DSpace on 2018-08-27T20:04:59Z (GMT). No. of bitstreams: 1 2018_RosaniKristineParaísoGarcia.pdf: 2789550 bytes, checksum: a0492b8e4403e5caca30e09c36a2fa26 (MD5) Previous issue date: 2018-08-22 / Este estudo versa sobre a expressão da polidez na Língua de Sinais Brasileira (Libras ou LSB) e desenvolve-se pela análise de dados coletados em comunidade surda usuária de Libras. Assim como em qualquer língua, nas línguas de sinais há o uso de diferentes registros e “graus” de polidez. O objetivo geral do estudo é analisar os elementos linguísticos utilizados como recursos na expressão gramatical da polidez em Libras, tomando como ponto de partida o trabalho pioneiro de Brown e Levinson (1987 [1978]) e um capítulo que Ferreira Brito (1995) desenvolve sobre esse assunto. Como se trata de um tema que está na interface entre a gramática e o discurso, a abordagem teórica leva em conta categorias de análise de base funcionalista, mas trabalha, também, com pressupostos da gramática gerativa, quanto à existência de uma faculdade da linguagem e de mecanismos gramaticais universais para a expressão do pensamento. O caminho metodológico adotado para esta pesquisa baseia-se em coleta de dados, por meio de filmagens em vídeo e de entrevistas, a fim de comparar os diferentes mecanismos gramaticais utilizados pelos surdos sinalizantes de Libras e analisar esses mecanismos com base no referencial teórico adotado. A análise dos dados permitiu identificar que os surdos participantes da pesquisa relacionam os registros formais e informais com o comportamento mais (ou menos) polido dos interlocutores, sendo a estrutura diretiva a preferida tanto em situações formais quanto em situações informais. Essa característica se revelou ser própria da Libras – confirmando-se a proposta de Ferreira Brito (1995) de que a familiaridade é um aspecto fundamental para a descrição da polidez nessa língua, e desafiando-se a teoria de Brown e Levinson (1987 [1978]) de que os atos de fala indiretos agregam elementos de polidez nas línguas em geral. / This research deals with the expression of politeness in Brazilian Sign Language (Libras or LSB) and is developed by the analysis of data produced by deaf people who are Libras’ speakers. Just as in any language, in sign languages different registers and degrees of politeness are used. The general objective of this study is to analyze the linguistic elements used as resources in the grammatical expression of politeness in Libras, taking as a start point Brown e Levinson’s (1987 [1978]) research and the chapter that Ferreira Brito (1995) developed on this subject. As this work deals with a theme that is at the interface between grammar and discourse, the theoretical approach takes into account categories of functionalist framework, but also the assumptions of generative grammar, about the existence of a language faculty and of universal grammatical mechanisms for the expression of thought. The methodological approach adopted for this research is based on data collected in order to compare the different grammatical mechanisms used by the deaf people and to analyze these mechanisms based on the adopted theoretical framework. The analysis allowed us to identify that the deaf participants relate formal and informal registers to the more (or less) polite behavior of the interlocutors, the directive structure being preferred in both formal and informal situations. This characteristic was considered to be proper of Libras – confirming the proposal of Ferreira Brito (1995) that familiarity is a fundamental aspect for the description of politeness in this language, and challenging the theory of Brown and Levinson (1987 [1978]) that the indirect speech acts generally show elements of politeness in the languages.

Esta dissertação é o resultado do meu verouvirsentir e busca evidenciar que, nas relações desenvolvidas no processo do ensino da matemática, as histórias em quadrinhos podem-se revelar um instrumento eficaz para a aplicação de uma metodologia alternativa dotada de uma potência extraordinária na interlocução entre a criança e o conteúdo matemático. Nesse contexto, um dos maiores argumentos que encontro, ao final desta jornada, é que fica a percepção de que o livro didático adotado (referência para o conteúdo teoricoprático), em quase sua totalidade, não favorece que os alunos estabeleçam uma relação com a matemática pautada na atenção, curiosidade, alegria e outros fatores/elementos que permitam o crescimento cognitivo desses alunos na referida disciplina. A pesquisa é realizadasentida em uma escola particular de ensino fundamental e médio situada em Realengo em três turmas de 6 ano. Esses alunos variam entre 10 e 13 anos de idade e aproximadamente 90% deles são oriundos de famílias de classe média. Para realizarsentir esta pesquisa, percebo que, fundamentalmente, faço uso de duas metodologias que se revelam a priori: pesquisa-ação e o mergulho (ALVES, 2008). Realizo alguns diálogos que se consolidam como aporte teórico e que norteiam toda a minha escrita. Esses diálogos podem ou não aparecer nas citações que faço. Os diálogos invisibilizados pela minha escrita de modo algum foram menos importantes e tampouco são considerados menos relevantes, na verdade, conduzem minha escrita, misturando-se em minhas próprias palavras a ponto de se tornarem indissociáveis. Nesses diálogos, encontro-me com Michel de Certeau, Paulo Sgarbi, Nilda Alves, Humberto Maturana, Inês Barbosa, Von Foerster, Michel Focault, Edgard Morin, Will Eisner, Ginsburg, entre outros. Como resultados, ficou evidenciado que, ao oferecer a possibilidade de reescrita da teoria matemática através das histórias em quadrinhos, os alunos (na sua maioria) desenvolveram uma capacidade maior de concentração, atenção aos detalhes da própria teoria e a diminuição significativa da resistência ao conteúdo matemático. Uma velhanova linguagem? Em um velhonovo meio? Seja qual for a conclusão, a aventura do desafio na busca da construção de uma nova relação entre a criança e a matemática, por si só, permite a exposição de tensões e oportuniza o crescimento de todos. Nessa jornada, de ação em ação, busco fazer algo significativo. / This dissertation is the result of my seelistenfeel seach to evidence that the relationships developed in the teaching of mathematics, the comic may prove an alternative methodology endowed with an extraordinary power in the dialogue between the child and mathematical content. In this context, one of the biggest arguments against the end of this journey is that the perception is that the textbook adopted (reference to theoretical and practical content) in almost its entirety, does not help students establish a relationship based in the mathematics attention, curiosity, joy and other factors/elements that allow the cognitive growth of students in that discipline. The search is performed in an experienced private school located in primary and secondary Realengo in three classes of Year 6. These students range between 10 and 13 years old and approximately 90% of these students come from middle class families. To feelperform this research experience, I realize that I basically use two methodologies that show the a priori: action research and diving (ALVES, 2008). I realize some dialogues that are consolidated as a theoretical basis and guiding all my writing. These dialogues may or may not appear in quotes I do. The dialogues obscured by my writing at all were less important, and neither are considered less relevant, in fact, lead my writing, mixing in my own words as to become inseparable. In these dialogues, I am met with Michel de Certeau, Paul Sgarbi, Nilda Alves, Humberto Maturana, Ines Bar-bosa, Von Foerster, Michel Foucault, Edgard Morin, Will Eisner, Ginsburg and others. As a result, it became evident that by offering the possibility of rewriting the mathematical theory through the comics, the students (mostly) developed a greater capacity for concen-tration, attention to detail of the theory itself and a significant decrease in resistance to mathematical content. An oldnew language? In a newold way? Whatever the conclusion, the adventure in search of the challenge of building a new relationship between the child and mathematics, by itself, allows the display of tensions and nurture the growth of all. Along the way, the action in action, I try to do something meaningful.

Abordagens clássicas de linguagens de consultas para bancos de dados possuem certas restrições ao serem usadas, diretamente, por aplicações que acessam dados cujo conteúdo não é completamente conhecido pelo usuário. Essas restrições geram um cenário onde argumentos de consultas, especificados com operadores boleanos, podem retornar resultados vazios. Desse modo, o usuário é forçado a refazer suas consultas até que os argumentos usados estejam idênticos aos dados armazenados no banco de dados. Em bases XML, este problema é reforçado pela heterogeneidade das formas em que a informação encontra-se armazenada em diferentes lugares. Como solução, uma alternativa seria o uso de funções de similaridade na substituição de operadores boleanos, a fim de que o usuário obtenha resultados aproximados para a consulta especificada. Neste trabalho é apresentada uma proposta para suporte a argumentos de consulta vagos através da extensão da linguagem XPath. Para isso, são utilizadas expressões XPath que utilizam novas funções, as quais são, diretamente, adicionadas ao processador da linguagem de consulta. Além disso, é apresentada uma breve descrição das métricas de similaridade utilizadas para a criação das funções. As funções que foram adicionadas a um processador XPath possuem uma ligação muito estreita com as métricas utilizadas. Como as métricas, as funções trabalham com valores simples (elementos atômicos) e compostos (elementos complexos). As funções que trabalham com elementos atômicos podem ser classificadas tanto pelo tipo de dado que será analisado, como pelo tipo de análise que será feita. As funções para elementos complexos comparam conjuntos de elementos atômicos de acordo com a forma do agrupamento (conjunto, lista ou tupla).

Submitted by Amanda Silva (amanda.osilva2@ufpe.br) on 2015-04-15T14:27:54Z No. of bitstreams: 2 Dissertação Camila Brito de Vasconcelos.pdf: 15904876 bytes, checksum: e27de644b4dfe4d76419338a305bc40c (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-04-15T14:27:54Z (GMT). No. of bitstreams: 2 Dissertação Camila Brito de Vasconcelos.pdf: 15904876 bytes, checksum: e27de644b4dfe4d76419338a305bc40c (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Previous issue date: 2014 / O projeto “A PERCEPÇÃO DOS SISTEMAS SIMBÓLICOS E LINGUAGENS VISUAIS DOS LADRILHOS HIDRÁULICOS EM PATRIMÔNIOS RELIGIOSOS TOMBADOS PELO IPHAN NA CIDADE DO RECIFE” dedica-se ao problema da preservação da memória visual em patrimônios culturais e artefatos históricos em Pernambuco. Propõe uma investigação das significações e contextos que envolvem os ladrilhos hidráulicos dos patrimônios históricos e culturais pernambucanos. A investigação das linguagens visuais e memória gráfica nos ladrilhos hidráulicos apresenta ao design a observação desses sistemas simbólicos. Por isso este projeto investiga as linguagens visuais e o resgate dos sistemas simbólicos presentes nos ladrilhos hidráulicos de patrimônios religiosos tombados pelo IPHAN na cidade do Recife. O projeto parte da ideia de que o design, em seus estudos de memória gráfica, pode atuar conjuntamente com a noção de patrimônio no Brasil, mais especificamente na cidade do Recife, preservando a memória visual de bens tombados que fazem parte do contexto das cidades, dos espaços construídos e consequentemente dos sujeitos observadores que constroem essas memórias.

Submitted by Daniella Sodre (daniella.sodre@ufpe.br) on 2015-04-17T14:15:28Z No. of bitstreams: 2 TESE Jucimar Maia da Silva Júnior.pdf: 4954306 bytes, checksum: fbddc0017ae748afd4a4afa5751c4a17 (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-04-17T14:15:28Z (GMT). No. of bitstreams: 2 TESE Jucimar Maia da Silva Júnior.pdf: 4954306 bytes, checksum: fbddc0017ae748afd4a4afa5751c4a17 (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Previous issue date: 2013-07-31 / Jogos via Internet, redes sociais e as novas aplicações web demandam acesso simultâneo e interativo de milhares (às vezes milhões) de pessoas. Esses sistemas são quase sempre desenvolvidos usando linguagens de script como PHP ou usando frameworks baseados em linguagens como Java, Ruby ou Pyhton. À proporção que o acesso a esses sistemas cresce, os fornecedores de tais serviços necessitam atender a novas demandas por meio da substituição de hardware por modelos mais potentes, aumentando seus custos operacionais. Quando o nível de acesso cresce drasticamente, o projetista se vê forçado a reprojetar toda a arquitetura do sistema migrando para soluções complexas usando Java Enterprise Edition (JEE) ou Node.js. Essas soluções também demandam mais e mais servidores. O problema possui uma raiz mais profunda: as linguagens de programação usadas para o desenvolvimento de sistemas não foram projetadas para suportar concorrência massiva. Linguagens com suporte a concorrência baseadas no modelo de memória compartilhada não possuem a escalabilidade necessária para atender a demanda. Para resolver os problemas ocasionados pela concorrência massiva, os desenvolvedores estão optando por usar linguagens funcionais como Scala e Erlang na arquitetura do sistema ao contrário de linguagens orientadas a objetos como Java. Mas Erlang não possui uma sintaxe própria para programação orientada a objetos. Este trabalho mostra o desenvolvimento de uma extensão orientada a objetos para a linguagem Erlang, chamada ooErlang, que possui uma melhor expressividade para resolução de problemas “do mundo real” e que não degrade o bom desempenho da linguagem em aplicações que demandam alto tráfego de dados e fina granularidade computacional, tal qual em programas Web 2.0. Assim sendo, o nicho da extensão aqui apresentada é o mesmo de Erlang: desenvolver sistemas backend para grandes aplicações onde a concorrência massiva e tolerância a falhas são requeridas.

Made available in DSpace on 2014-06-12T15:59:19Z (GMT). No. of bitstreams: 2 arquivo5030_1.pdf: 2680874 bytes, checksum: e4a9926df270ffa311253fe6fe777efc (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2002 / A fim de tornar os sistemas Web mais robustos, a construção de testes de softwares Web e sua automação vêm sendo enfatizadas por metodologias de desenvolvimento. A metodologia Extreme Programming (XP), por exemplo, tem destacado a atividade de teste (em particular, os testes de aceitação e de unidade) como uma das práticas de programação chaves para o sucesso de sua implantação, sendo a construção destes testes realizada antes mesmo da implementação do código testado. Apesar de ter suas vantagens reconhecidas, a atividade de teste é na maioria das vezes ignorada ou apenas parcialmente realizada, principalmente quando deixado para o final do desenvolvimento. Sendo mais um esforço para o incentivo da realização de testes de sistemas Web, em particular os testes de aceitação, este trabalho tem como objetivo definir uma linguagem para descrição de casos de teste de aceitação com alto nível de abstração e reuso. Para dar suporte a utilização desta linguagem, objetivamos a criação de um ambiente de execução para a mesma. Além disto, este trabalho também estuda a criação de possíveis geradores de código que possam ser utilizados para amenizar o impacto negativo na produtividade, a curto prazo, causado pela realização dos testes de aceitação. Estes geradores dão suporte a criação destes testes antes da implementação do próprio sistema, prática apresentada pela metodologia

Made available in DSpace on 2014-06-12T15:59:30Z (GMT). No. of bitstreams: 2 arquivo5132_1.pdf: 1120699 bytes, checksum: d826be5393b747d7f2d6eec4b73a8ba4 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2006 / Uma abordagem para controlar os erros de resultados de computações numéricas é utilizar a Matemática Intervalar. A Matemática Intervalar é uma teoria matemática que propõe solucionar problemas relacionados às inexatidões e imprecisões que aparecem na computação científica. Dessa maneira, a utilização de técnicas intervalares é uma alternativa para alcançar limites garantidos para os resultados de computações. Portanto, este trabalho tem como objetivos (i) implementar uma biblioteca XSC para suprir as necessidades de Java relacionadas com a implementa;ao dos números reais através dos números de ponto flutuante e (ii) desenvolver uma calculadora intervalar que resume e permite o uso das operações aritméticas, lógicas, transcendentais, trigonométricas e estatísticas que compõe a biblioteca intervalar Java. As facilidades da linguagem Java, entre elas reuso e aspectos de herança, permitiram o desenvolvimento modular e robusto da biblioteca intervalar. Quando comparados como o software IntpakX, os resultados obtidos com a calculadora Java-XSC foram satisfatórios considerando a métrica distância

Made available in DSpace on 2014-06-12T15:59:39Z (GMT). No. of bitstreams: 2 arquivo5428_1.pdf: 1146136 bytes, checksum: 397adc67935622083166ac6104064af6 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2006 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / A busca constante pelo desenvolvimento de sistemas de software com qualidade vem despertando o interesse das grandes empresas na aplicação de técnicas formais. Dentre as linguagens formais, existem aquelas próprias para a modelagem de dados complexos, tal como Z, e outras próprias para a modelagem de comunicação e concorrência, tal como CSP. Circus é uma linguagem de especificação, projeto e programação que combina Z e CSP. Além de possibilitar a especificação de aspectos de dados e comportamentais de sistema concorrentes, Circus inclui um cálculo de refinamentos. Este é seu diferencial em relação a outras integrações de Z com uma álgebra de processos. Circus vem despertando interesse no meio industrial, manifestado através de colaboraçõoes científicas e tecnológicas, e possui uma equipe envolvida na construção de ferramentas que visam facilitar sua utilização. Muitas destas ferramentas precisam de um verificador de tipos para prover mais garantias quanto a consistência das especificações e programas, e, consequentemente, de seus resultados. Neste trabalho, apresentamos uma definição formal para o sistema de tipos de Circus, com o intuito de auxiliar o desenvolvimento de um verificador de tipos para a linguagem. Optamos por primeiramente definir as regras de tipos de Circus para depois implementar o software que automatiza a aplicação dessas regras. Esta decisão de projeto contribuiu para a construção robusta do verificador, pois a implementação consiste em um mapeamento direto das regras de tipos para linhas de código. O verificador desenvolvido também oferece recursos adicionais, tais como, a disponibilidade de informações de tipos para cada fragmento da especificação ou programa passado para análise, e o fornecimento de mensagens claras e objetivas dos possíveis erros de tipos detectados ao longo da verificação. Adicionalmente, projetamos o verificador como um componente de fácil integração, manutenção e extensão. Também apresentamos neste trabalho a nossa estratégia de validação do verificador. Elaboramos testes de pequeno e grande porte, a partir de estudos de casos de sistemas reais, tal como o sistema de SmartCard que descrevemos neste trabalho. Adicionalmente, integramos o verificador com outra ferramenta: o JCircus, que é um tradutor de Circus para Java. Também implementamos uma versão inicial de uma ferramenta de refinamentos, chamada CircusRefine, para integrar o verificador de tipos. Apesar de não termos construído uma versão completa de CircusRefine, nos preocupamos em definir a arquitetura da ferramenta de tal forma que sejam possíveis futuras evoluções de forma simples e estruturada. Os testes e integrações contribuíram para a correção de defeitos da implementação e para a evolução e verificação de consistência do verificador de tipos de Circus. Ao definir o sistema de tipos de Circus, e disponibilizar um verificador de tipos, acreditamos que estamos dando uma importante contribuição na evolução de Circus, esclarecendo pontos essenciais de sua definição como uma linguagem fortemente tipada e compatível com Z e CSP, e estamos também contribuindo para o desenvolvimento de outras ferramentas da linguagem.Esperamos que o nosso trabalho possa servir de base para a definição e implementação dos sistemas de tipos das extensões de Circus

Made available in DSpace on 2014-06-12T16:00:51Z (GMT). No. of bitstreams: 2 arquivo7069_1.pdf: 2309680 bytes, checksum: 9f82816fc4ec4e7c3d5e9a9fec8419fe (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2011 / Em sistemas embarcados, uma de suas partes críticas é o escalonador de tarefas. Este é responsável por determinar qual tarefa ocupará o processador em cada instante de tempo. Uma escolha de tarefa errada pode ter resultados que vão de uma diminuição de desempenho à perda de vidas humanas. Diante de sistemas cada vez mais complexos, surge a necessidade de criar escalonadores de tarefas especializados para aplicações específicas com o intuito de melhorar o desempenho desses sistemas. Sendo a implementação de escalonadores uma tarefa trabalhosa, que requer o uso de linguagens de baixo nível, esse trabalho de mestrado apresenta uma linguagem específica de domínio, a SchedLanguage, para facilitar a implementação de políticas de escalonamento dirigidas a prioridades. Com uma sintaxe simples, a SchedLanguage facilita a implementação de escalonadores, permitindo que estes sejam especificados em um nível de abstração maior. Além disso, também proporciona uma detecção precoce de erros relacionados ao entendimento e definição do sistema. Também é mostrado neste trabalho a ferramenta SchedTool, que gera um escalonador a partir de uma especificação em SchedLanguage. A utilização da linguagem proposta neste trabalho não é restrita a uma única plataforma. Por necessitar de algumas informações relacionadas à plataforma utilizada, uma mesma especificação nessa linguagem pode ser utilizada em diferentes plataformas. A linguagem e a ferramenta apresentadas neste trabalho foram validadas utilizando uma plataforma de referência ArchC, sendo utilizadas para escalonar diferentes tipos de tarefas

Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2017-08-23T12:57:53Z No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) Dissertacao_Heitor_Maranhao.pdf: 1117044 bytes, checksum: ceea86d5a4dad585b8f79f5f79278656 (MD5) / Made available in DSpace on 2017-08-23T12:57:53Z (GMT). No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) Dissertacao_Heitor_Maranhao.pdf: 1117044 bytes, checksum: ceea86d5a4dad585b8f79f5f79278656 (MD5) Previous issue date: 2016-09-13 / Program synthesis aims to automate the task of programming. Through program synthesis it is possible to let the programmer free to care about the description (specification) of the problem to be solved by the program under development, reducing human interaction with coding tasks. Automating new algorithms creation and transferring responsibility for writing code are some of the benefits propitiated by program synthesis. In this work, program synthesis is presented as an Alloy* specification for an imperative language. We synthesize programs described by pre and post-conditions (contracts) written using a Domain Specific Language proposed in this work. We embed the syntax and the denotational semantics of Winskel’s imperative language in Alloy*. Alloy* has proven to be an easy and productive way of building program synthesizers. Our experiments show that synthesis based on Alloy* is competitive once contracts, scopes and, if needed, sketches, are correctly chosen. As a consequence, our Alloy* program synthesizer can provide, in a single high-level framework, different features in comparison to other synthesizers: (i) synthesis based on scope; (ii) synthesis based on sketches; and (iii) verification. We introduce our Domain Specific Language for contracts and present a detailed description on the synthesis of the swap problem, the product of two numbers, the maximum of 2 and of 3 numbers, and the greatest common divisor. Another contribution of this work is a source code generator, using the programming language C#, of the algorithms created by our synthesizer. / Síntese de programas permite automatizar as atividades de programação. Através desta automação é possível deixar o programador livre para criar a descrição (especificação) do problema que o programa a ser desenvolvido busca resolver, reduzindo a interação humana com a etapa de escrita de código. Automatizar criação de novos algoritmos e transferir para máquinas a responsabilidade de escrever o código de programas são alguns dos benefícios que a síntese de programas possibilita. Neste trabalho, síntese de programas é apresentada através de uma especificação em Alloy* usando uma linguagem imperativa. A síntese é realizada a partir de um par de predicados, pré e pós-condição (contrato), escritos usando uma linguagem de domínio específico proposta neste trabalho. A semântica denotacional da linguagem imperativa usada por Winskel foi embutida em Alloy*. O uso de Alloy* se mostrou uma maneira fácil e produtiva de construir sintetizadores de programas. Os experimentos mostram que síntese baseada em Alloy* é competitiva, uma vez que contratos, escopos e, se necessário, esboços, sejam corretamente escolhidos. Como consequência, o sintetizador de programas em Alloy* pode fornecer, em um único framework de alto nível, características diferentes em comparação com outros sintetizadores: (i) síntese baseada em escopo; (ii) síntese baseada em esboços; e (iii) verificação. Para demonstrar a aplicabilidade prática de nosso trabalho, usamos nossa ferramenta na síntese de problemas clássicos da Computação, tais como troca do valor entre duas variáveis, o produto de dois números, o máximo de 2 e 3 números, e o maior divisor comum entre dois números. Outra contribuição deste trabalho consiste em um gerador de código na linguagem de programação C#, dos algoritmos criados pelo nosso sintetizador.