JavaCO – uma variante do Java com um sistema de tipos baseado em covariância

Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para obtenção do grau de Mestre em Engenharia Informática

Falsos amigos PT-SP en el lenguaje jurídico - una propuesta de clasificación

Comunicação apresentada nas Jornadas de Língua e Direito, organizadas pelo ISCAP e pela Universidade Católica Portuguesa, Outubro de 2013.

Linguagem de especificação leve Hoare-separação para java

Trabalho apresentado no âmbito do Mestrado em Engenharia Informática, como requisito parcial para obtenção do grau de Mestre em Engenharia Informática

Service-oriented mobility of java code in web services-based architectures

Dissertação apresentada na Faculdade de Ciências e Tecnologias da Universidade Nova de Lisboa para a obtenção do Grau de Mestre em Engenharia Informática

JAVA Applets, um comboio em início de marcha

Java! Uma palavra nova e misteriosa que consegue conjugar imagens, movimento, internet, programação, café quente e o nome de uma das 10,000 ilhas dos nossos amigos da Indonésia. No entanto, é sobre os quatro primeiros conceitos que se trata este projecto de “JAVA Applets, um comboio em início de marcha”. Se o HTML vem ligar imagens à internet, o JAVA tenta dar uma certa interactividade utilizando programação mas, tentando também, que os utilizadores finais a possam utilizar sem grande esforço.

Avaliação dos mecanismos de concorrência na API do Java 8

As plataformas com múltiplos núcleos tornaram a programação paralela/concorrente num tópico de interesse geral. Diversos modelos de programação têm vindo a ser propostos, facilitando aos programadores a identificação de regiões de código potencialmente paralelizáveis, deixando ao sistema operativo a tarefa de as escalonar dinamicamente em tempo de execução, explorando o maior grau possível de paralelismo. O Java não foge a esta tendência, disponibilizando ao programador um número crescente de bibliotecas de mecanismos de sincronização e paralelização de código. Neste contexto, esta tese apresenta e discute um conjunto de resultados obtidos através de testes intensivos à eficiência de algoritmos de ordenação implementados com recurso aos mecanismos de concorrência da API do Java 8 (Threads, Threadpools, ExecutorService, CountdownLach, ExecutorCompletionService e ForkJoinPools) em sistemas com um número de núcleos variável. Para cada um dos mecanismos, são apresentadas conclusões sobre o seu funcionamento e discutidos os cenários em que o seu uso pode ser rentabilizado de modo a serem obtidos melhores tempos de execução.

Type-based protocol conformance and aliasing control in concurrent java programs

Dissertação para obtenção do Grau de Mestre em Engenharia Informática

Data-centric concurrency control on the java programming language

Dissertação para obtenção do Grau de Mestre em Engenharia Informática

Los efectos de la transposición didáctica en la enseñanza del lenguaje escrito

En el presente proyecto se pretende explorar si los textos que se requieren a los alumnos responden a las características y exigencias de los textos de mayor circulación social que supuestamente serán requeridos por la sociedad una vez que los niños egresan de la etapa de escolaridad obligatoria. Un primer análisis de los textos escritos por los alumnos, registrados en sus cuadernos como "tareas de composición" permitió observar transformaciones sustanciales que los distancian notablemente de las características y estructuras esenciales definidas por la lingüística textual y la pragmática discursiva. El objetivo de este estudio es analizar la distancia que separa los textos escolares de los textos sociales desde una perspectiva de los estudios actuales de transposición didáctica. Se caracteriza a la transposición didáctica como un proceso complejo de transformaciones adaptativas mediante el cual el conocimiento elaborado en el plano científico se convierte en conocimiento escolarizado. En el proyecto se propone explorar las transformaciones que se producen en la enseñanza del lenguaje escrito, focalizando el análisis en dos planos: 1. El plano textual pretende: detectar la distancia que se produce en el contexto de producción y los textos de circulación social con las condiciones de producción efectivamente por los alumnos. Además, comparar las características configuracionales y discursivas que identifican a los textos sociales y escolares. 2. Plano ortográficos tal como son descriptos por la disciplina de referencia y como son vehiculizados en el aula. Interesa elaborar categorías de transposición didáctica al lenguaje escrito, planos de análisis para describir las transformaciones que se producen durante el proceso de pedagogización del saber. Al evidenciar las transformaciones que se infringe al lenguaje escrito como consecuencia de ciertas prácticas pedagógicas, se pretende contribuir a repensar las mismas con el propósito de neutralizar los efectos distorsionantes de la transposición didáctica.

Sistemas de Tipos para Verificación de Programas Concurrentes. Type Systems for Concurrent Programs Verification.

La programación concurrente es una tarea difícil aún para los más experimentados programadores. Las investigaciones en concurrencia han dado como resultado una gran cantidad de mecanismos y herramientas para resolver problemas de condiciones de carrera de datos y deadlocks, problemas que surgen por el mal uso de los mecanismos de sincronización. La verificación de propiedades interesantes de programas concurrentes presenta dificultades extras a los programas secuenciales debido al no-determinismo de su ejecución, lo cual resulta en una explosión en el número de posibles estados de programa, haciendo casi imposible un tratamiento manual o aún con la ayuda de computadoras. Algunos enfoques se basan en la creación de lenguajes de programación con construcciones con un alto nivel de abstración para expresar concurrencia y sincronización. Otros enfoques tratan de desarrollar técnicas y métodos de razonamiento para demostrar propiedades, algunos usan demostradores de teoremas generales, model-checking o algortimos específicos sobre un determinado sistema de tipos. Los enfoques basados en análisis estático liviano utilizan técnicas como interpretación abstracta para detectar ciertos tipos de errores, de una manera conservativa. Estas técnicas generalmente escalan lo suficiente para aplicarse en grandes proyectos de software pero los tipos de errores que pueden detectar es limitada. Algunas propiedades interesantes están relacionadas a condiciones de carrera y deadlocks, mientras que otros están interesados en problemas relacionados con la seguridad de los sistemas, como confidencialidad e integridad de datos. Los principales objetivos de esta propuesta es identificar algunas propiedades de interés a verificar en sistemas concurrentes y desarrollar técnicas y herramientas para realizar la verificación en forma automática. Para lograr estos objetivos, se pondrá énfasis en el estudio y desarrollo de sistemas de tipos como tipos dependientes, sistema de tipos y efectos, y tipos de efectos sensibles al flujo de datos y control. Estos sistemas de tipos se aplicarán a algunos modelos de programación concurrente como por ejemplo, en Simple Concurrent Object-Oriented Programming (SCOOP) y Java. Además se abordarán propiedades de seguridad usando sistemas de tipos específicos. Concurrent programming has remained a dificult task even for very experienced programmers. Concurrency research has provided a rich set of tools and mechanisms for dealing with data races and deadlocks that arise of incorrect use of synchronization. Verification of most interesting properties of concurrent programs is a very dificult task due to intrinsic non-deterministic nature of concurrency, resulting in a state explosion which make it almost imposible to be manually treat and it is a serious challenge to do that even with help of computers. Some approaches attempts create programming languages with higher levels of abstraction for expressing concurrency and synchronization. Other approaches try to develop reasoning methods to prove properties, either using general theorem provers, model-checking or specific algorithms on some type systems. The light-weight static analysis approach apply techniques like abstract interpretation to find certain kind of bugs in a conservative way. This techniques scale well to be applied in large software projects but the kind of bugs they may find are limited. Some interesting properties are related to data races and deadlocks, while others are interested in some security problems like confidentiality and integrity of data. The main goals of this proposal is to identify some interesting properties to verify in concurrent systems and develop techniques and tools to do full automatic verification. The main approach will be the application of type systems, as dependent types, type and effect systems, and flow-efect types. Those type systems will be applied to some models for concurrent programming as Simple Concurrent Object-Oriented Programming (SCOOP) and Java. Other goals include the analysis of security properties also using specific type systems.

JAVADAPTOR : unrestricted dynamic updates of Java applications

In dieser Arbeit wird mit JAVADAPTOR ein Ansatz präsentiert, der die statisch getypte Programmiersprache Java um die Möglichkeit erweitert, Programme zur Laufzeit und ohne die genannten Einschränkungen zu aktualisieren. Das vorgestellte Konzept kombiniert das schemaverändernde Nachladen von Klassen mit Referenzaktualisierungen auf der Basis von Java HotSwap, Containern und Proxies. Zentrale Beiträge der Arbeit sind detaillierte Beschreibungen der Konzepte und deren Implementierung, sowie der Nachweis der Praxvistauglichkeit der Lösung anhand verschiedener Fallstudien. Weiterhin wird untersucht, ob die präsentierte Lösung Einschränkungen bezüglich Flexibilität, Performanz, Plattform, Programmarchitektur oder Änderungsgranularität unterliegt.