Semântica de Java
Java and the Java Virtual Machine - Definition, Verification,
Validation
Robert Stark, Joachim Schmid, and Egon Borger
Wolfram Schulte
DI
UFPE
Introdução

Objetivos
 Definição
 Base
rigorosa, mas legível
para padronização de Java (ambiguidades e
inconsistencias foram detectadas)
 Especificação
e avaliação de extensões de Java
 Análise
e comparação de implementações de Java
 Modelo
passível de tratamento automático
 Validação
de esquemas de compilação e de
propriedades de segurança
DI
UFPE
Introdução


DI
UFPE
Requerimentos
 Validação por inspeção
 Técnica de modelagem que:
 Expresse conceitos básicos
 Modele ações básicas de forma abstrata
Abstract State Machines (ASM)
 Gurevich- Evolving Algebras
 Semântica operacional em que estados são
definidos algebricamente
 Pseudo-code envolvendo tipos de dados abstratos
Introdução

Interpretador de programas Java
 “Parsing”
 Elaboração:
tipos e formação
 Execução

Carga, ligação e execução

Semântica dinâmica
 Jumps
 Exceções
 Concorrência
DI
UFPE
Introdução


DI
UFPE
Características do modelo
 Orientado a processo ao invés da sintaxe
 Separação de aspectos estáticos e dinâmicos
Métodos estruturados
 Semântica operacional estruturada, semântica natural,
semântica de ações, etc.
 Adequados para linguagens cujo fluxo de controle segue
a árvore sintática
 Nenhuma vantagem quando:
 Ambientes são mais complexos
 Concorrência é considerada
Abstract State Machines

Estado: estrutura matemática

Conjunto de regras de transição da forma
if Condition then Updates

Condition: predicado

Updates: conjunto de
f(t1,...,tn) := t

DI
UFPE
Execução: noção tradicional
Abstract State Machines
Tipos de Funções

Estáticas

Dinâmicas
 Controladas
 Monitorada
 Interativas
 Derivadas
DI
UFPE
Abstract State Machines
Formas Especiais de Regras



DI
UFPE
forall x with Condition do Rule
choose x with Condition do Rule
Além disso
 where
 let
 if then else
 Parametrização
Visão geral

Cinco sublinguagens
 Isolamento
DI
UFPE
de características ortogonais

Imperativas - JavaI

Procedimentais (baseadas em objetos) - JavaC

Orientadas a objetos - Javao

Tratamento de exceções - JavaE

Concorrência - JavaT
JavaI


DI
UFPE
Sintaxe
 Página 35, Figura 3.1
 Programa anotado, como em tempo de execução
Modelo de execução
 Passeio pelos nós da árvore sintática de um
programa
 Em cada nó
 Uma tarefa é executada
 Prosseguimento para a próxima tarefa
JavaI
Estado
DI
UFPE

Contador de programas abstrato: programa a ser
executado
pos : Pos
restbody: Pos  Phrase

Ambiente
locals: Locals
type Locals = Map(Loc  Val)

Estado: restbody, post, locals
JavaI
Transições



DI
UFPE
Regras de transição: mudanças de estado devido a
 Avaliação de expressões
 Execução de comandos
Estado inicial
 Determinado por uma phrase dada
 restbody = a frase
 pos = posição inicial
 locals vazio
Execução termina: nenhuma regra é aplicável
JavaI
Expressões

DI
UFPE
Expressões
 Ordem de avaliação
 Da esquerda para direita, de dentro para fora
 context e yield e yieldUp
 Figura 3.2, página 41
JavaI
Comandos

DI
UFPE
Figura 3.3, página 42
JavaC

Linguagem com módulos

Sintaxe: páginas 48- 49, Figura 4.3, página 50, 51-52
 Informações

Ambiente de classes estático
 Definido
DI
UFPE
de tipo já inseridas em tempo de compilação
por funções: página 62
JavaC
Estado

Mais componentes de estado
 initialized
 globals

Chamada de métods
 type
Frame = (Class/Msig, Phrase,Pos,Locals)
 frames:

DI
UFPE
Frame*
Mais Abr para mudança abrupta de fluxo
JavaC
Regras de Transição

Todas as regras de JavaI com

Ambiente definido pelo programa dado

Todos os atributos inicializados com valores “default”

Início
 public
 body,
DI
UFPE
static void main()
restbody, pos, locals
JavaC
Regras de Transição

Expressões
 Figura

Comandos

DI
UFPE
4.4, página 64
Figura 4.5, página 66
JavaC
Inicialização
DI
UFPE

Inicialmente nenhuma classe é inicializada

Inicialização ocorre no primeiro uso ativo

Superclasses devem ser inicializadas antes

O mesmo não ocorre com superinterfaces
JavaO




DI
UFPE
Sintaxe: Figura 5.1, página 73
Ambiente
 instanceFields
 defaultVal
 type
 lookup
Estado
 type Val = ... | Ref | Null
 data Heap = Object(Class,Map(Class/Field,Val))
 heap: Ref  Heap
Regras de transição: Figura 5.2, página 81
JavaE

Sintaxe: Figura 6.1, página 88

data Abr = Break(Lab) | Continue(Lab) |
Return | Return(Val) | Exc(Ref)

DI
UFPE
Regras de transição:
 Figura
6.2, página 91
 Figura
6.3, página 93