lista Exercicios Alloy

Prévia do material em texto

Considerando o modelo Alloy (abaixo) para representar um subconjunto da linguagem de
programação Java, responda os questionamentos que se seguem.
module javametamodel_withfield
open util/relation
abstract sig Id {}
sig ClassId, MethodId, FieldId, SequentialId extends Id {}
abstract sig Accessibility {}
one sig public, private_, protected extends Accessibility {}
abstract sig Type {}
abstract sig PrimitiveType extends Type {}
one sig Long_ extends PrimitiveType {}
abstract sig Class {
extend: lone ClassId,
methods: MethodId -> one Method,
fields: set Field
}
sig Field {
id: one FieldId,
type: one Type,
acc : one Accessibility
}
sig Method {
id: one MethodId,
return: lone Type,
acc: one Accessibility,
body: seq Statement
}
abstract sig Expression {}
abstract sig Statement extends Expression {}
abstract sig PrimaryExpression extends Expression {}
sig this_, super_ extends PrimaryExpression {}
sig newCreator extends PrimaryExpression {
id_cf : one ClassId
}
sig FieldAccess extends Statement{
pExp: one PrimaryExpression,
id_fieldInvoked: one FieldId
}
sig MethodInvocation extends Statement{
pExp: one PrimaryExpression,
id_methodInvoked: one MethodId
}
sig LiteralValue extends Expression {}
sig Program {
classDeclarations: ClassId -> one Class,
main: Method
}
1) por que em algumas assinaturas foi usada a palavra chave one ?
2) Considerando a conhecida semântica estática de Java, elabore um predicado que ,
quando avaliado, diga se um determinado programa (tipo Program) é bem formado (ex.:
não possui erros de compilação) na linguagem;
Dica1: um programa é bem formado quando as classes que o compõem também são
bem formadas. Uma classe é bem formada quando os elementos (métodos, atributos,
etc) que a compõem também são bem formados. E assim por diante, de acordo com os
elementos que estão definidos no nosso modelo;
Dica2: Para resolver essa questão você deve utilizar todos os elementos definidos no
modelo.
Dica3: Use e abuse de predicados e funções auxiliares de forma que nenhum predicado ,
isoladamente, fique "grande" demais. Preze pela modularidade e simplicidade.
3) Elabore 5 assertions que checam se a semântica estática construída em 2 é preservada
no modelo.
Observação: todas as modificações solicitadas para o modelo nas questões abaixo, devem ser
realizadas através da confecção de fatos e/ou predicados e/ou assertions. Alterações na
definição dos tipos e suas respectivas relações não são permitidas.