Modelação de Software em Engª de Requisitos, João Pascoal Faria, ERSS, 2003 1 Modelação & Especificação de Sistemas de Software no contexto da Engenharia

Modelação de Software em Engª de Requisitos, João Pascoal Faria, ERSS, 2003 1

Modelação & Especificação de Sistemas de Software no contexto da Engenharia de Requisitos

João Pascoal Faria

Engenharia de Requisitos de Sistemas de Software

Versão 4.0 (partes I, II e III), 8/12/2003


Objectivo Saber criar modelos de sistemas de software

(representações em pequena escala a um nível elevado de abstracção) que permitam: 1. exprimir os requisitos dos sistemas de software como

propriedades nesses modelos, de forma o mais compreensível, completa, consistente e não ambígua possível (modelo como especificação completa, consistente e não ambígua de sistema a desenvolver)

2. verificar formalmente (por demonstração) a consistência interna do modelo e a obediência a propriedades (modelo formal)

3. testar (animar) o modelo para verificar a sua consistência interna e validar os requisitos o mais cedo possível (modelo executável)

4. verificar mais tarde a conformidade da implementação com o modelo/especificação (i.e., a obediência aos requisitos expressos no modelo)

5. servir de base para a construção/implementação do sistema (modelo traduzível, construtivo)


ÍndiceI. Introdução

II. Modelação visual (semi-formal) em UML

III. Modelação formal com OCL (Enriquecimento de modelos visuais em UML com

especificações formais de invariantes, pré-condições e pós-condições em OCL)

IV. Elaboração de modelos executáveis e traduzíveis em UML executável X

TUML (Enriquecimento de modelos visuais em UML com

especificações de acções em linguagem de alto nível)

V. Modelação / especificação formal em VDM++

VI. Verificação e validação baseada em modelos


Porquê modelos formais e executáveis? (1) Consensual e prática cada vez mais corrente:

• modelação visual com diagramas UML durante as fases de captura e especificação de requisitos, desenho de alto nível (arquitectura) e desenho detalhado

• geração de algum código (Java, C#, SQL, XSD, etc.) a partir de UML e vice-versa

Passos seguintes:• modelos como especificações completas e rigorosas (sem

ambiguidades nem inconsistências) de alto nível- especificar restrições formalmente (com invariantes)- especificar formalmente a semântica das operações (com pré e pós

condições) e, possivelmente, casos de utilização- importante para aumentar o rigor (complementando especificações

informais) - importante para suportar a verificação formal (do modelo e

conformidade da implementação)- uma especificação pretende ser declarativa (diz os objectivos) e não

necessariamente executável (não pretende dizer o caminho)- OCL e VDM++ são opções possíveis


Porquê modelos formais e executáveis? (2) Passos seguintes (cont.):

• modelos executáveis de alto nível- necessário especificar acções e algoritmos (resposta a

eventos, corpo de operações, ...), em linguagem de muito alto nível

- importante para validar os requisitos o mais cedo possível- Executable UML e VDM++ são opções possíveis

• geração automática de código completo (e não só esqueletos de classes) a partir de modelos de alto nível

- Executable UML e VDM++ são opções possíveis

VDM++ mais maduro e parcialmente integrado com UML, mas combinação de OCL e UML executável poderá ganhar


O que são métodos formais ? Método Formal =

Linguagem de Especificação Formal + Raciocínio Formal (verificação formal, ...)

As técnicas são suportadas por

• Matemática precisa

• Ferramentas de análise poderosas

Constituem um mecanismo rigoroso e efectivo para modelação, síntese e análise de sistemas

Especificação / modelo formal Implementação

síntese

análise

modelação/especificação


Classificação de métodos formais Baseados em Modelos

• Definem o comportamento do sistema através da construção de um modelo de dados (ou estado) usando estruturas matemáticas (conjuntos, sequências, funções finitas, etc.) - VDM, Z

• Particularmente apropriados para desenvolvimento de sistemas de informação

Baseados em Propriedades• Modelam tipos de dados implicitamente definindo o comportamento do

sistema através de um conjunto de propriedades• Algébricos – definem semântica de operações através de uma colecção de

relações de equivalência (axiomas equacionais) - Obj, Larch, ...• Axiomáticos – definem semântica de operações através de predicados da

lógica de primeira ordem - Larch, ...

Baseados no Comportamento• Definem sistemas em termos de sequências possíveis de estados em vez de

tipos de dados e são normalmente usados para especificar sistemas concorrentes e distribuídos

• Exemplos de formalismos: redes de Petri, Calculus of Communicating Systems (CCS), Communicating Sequencial Processes (CSP); lógica temporal; sistemas de transição; álgebras de processos


Exemplo em VDM++ (baseada em modelos)

class Stack instance variables elems : seq of int := []; operations Stack: () ==> () -- construtor Stack () == elems := [] post elems = []; Push : int ==> () Push(i) == elems := [i] ^ elems

post elems = [i] ^ ~elems; Pop : () ==> () Pop() == elems := tl elems

pre elems <> [] post elems = tl ~elems; Top : () ==> int Top() == return (hd elems)

pre elems <> [] post RESULT = hd elems

and elems = ~elems; end Stack

É necessário escolher uma representação do estado de uma stack!

Representação de dados (estado) baseada em construções matemáticas (conjuntos, sequências, funções finitas, etc.)!

Se fosse caso disso, podiam-se especificar invariantes, i.e., condições a que têm de obedecer os estados válidos.

Pós-condição é uma condição que relaciona o resultado da operação e o estado final do objecto com os argumentos de chamada e o estado inicial do objecto.

Corpo algorítmico

Pré e pós-condição especificam semântica da operação!

Pré-condição é uma condição (nos argumentos de chamada e estado inicial do objecto) a que tem de obedecer qualquer chamada válida.


Exemplo em OBJ (algébrica)Spec: Stack;

Extend Nat by

Sorts: Stack;

Operations:

newstack: Stack

push: Stack Nat Stack

pop: Stack Stack

top: Stack Nat

Variables:

s: Stack; n: Nat

Axioms:

pop(newstack) = newstack;

top(newstack) = zero;

pop(push(s,n)) = s;

top(push(s,n)) = n;

Mais abstracta: especifica semântica de operações por axiomas, sem necessidade de escolher uma representação de dados interna (cf. noção de ADT)!

Uma stack é sempre representada por uma expressão de construção, e.g.,

push(push(push(newstack, 1), 2), 3)

Axiomas permitem simplificar/avaliar expressões

top(pop(push(push(newstack, 1), 2))) =

= top(push(newstack, 1))

= 1












Modelação visual em UML Os modelos visuais são muito importantes

para facilitar a visualização e compreensão

Peças principais para captura e especificação de requisitos

• Modelo da arquitectura do sistema

• Modelo de casos de utilização

• Modelo de (objectos de) domínio


Modelo da arquitectura do sistema Só se justifica em sistemas complexos Decomposição em sub-sistemas, com indicação de

dependências entre sub-sistemas, e dependências em relação a sistemas externos

Cada sub-sistema corresponde a uma área funcional (grupo de funcionalidades), cobrindo todas as camadas da implementação (UI, BL, BD)

Os sub-sistemas podem por sua vez ser decompostos da mesma forma

Em UML, representar por diagrama de estrutura estática, com pacotes (packages) e sub-pacotes

• Possibilidade de indicar estereótipos «system» e «subsystem»

Em alternativa, representar por diagrama de blocos com ligações/fluxos entre blocos


Gestão de Cuidados de Saúde

Bloco OperatórioHospital de Dia

Urgência Consultas Internamento MCDT

Cuidados Comuns

Cuidados DiferenciadosCuidados Primários

Saúde Familiar Cuidados na Comunidade

Saúde Pública

Só contactos individualizados estarão registados no SIIMS

Exemplo: Sistema de Gestão de Cuidados de Saúde

sistema

sub-sistema

dependência


Modelo de casos de utilização Finalidade: mostrar a utilidade ou usos possíveis do

sistema

Conteúdo: actores (tipos de utilizadores e sistemas externos que interagem com o sistema), casos de utilização (funcionalidades do sistema tal como são vistas externamente, ou tipos de interacções entre actores e o sistema) e relações entre ambos

Casos de utilização capturam os requisitos funcionais e alguns requisitos não funcionais

Dificuldade: qual a granularidade dos casos de utilização?


Forma do modelo de casos de utilização (1) Visão geral

•Diagrama de casos de utilização acompanhado de descrição textual que passa superficialmente pelos casos de utilização e actores mais importantes


Autor-Submissor

Presidente do comité de programa

Revisor

Submeter Artigo

Sistema de Gestão de Conferências

Configurar sistema (dadosgerais da conferência, prazos,

temas e revisores)

Atribuir revisoresa artigos

Decidir aceitação ourejeição de artigos

Submeter versãofinal de artigo

Obter artigos pararever

Submeter revisões

Notificar revisores

«include»

Notificarautor-submissor

«include»

Exemplo: Sistema de Gestão de Conferências

actor

fronteira do sistema

nome do sistema

caso de utilização

diagrama de casos de utilização


Forma do modelo de casos de utilização (2) Visão geral (cont.)

•Se existirem muitos casos de utilização, apresentar um primeiro diagrama de pacotes de casos de utilização e depois um diagrama de casos de utilização para cada pacote

- Pacotes correspondem normalmente a sub-sistemas no modelo da arquitectura


Exemplo: Sistema de Gestão de Hotéis (CRM4SH) (1)

CRM4SH

Cliente

Recepcionista

Gerente

Público

Aplicação deGestão

Site Web

diagrama de pacotes de casos de utilização



CRM4SH - Site Web

Cliente

Público

Área para o público

Consultar características,serviços, preços edisponibilidades

Registar-se comocliente

Área para clientes registados

Alterar dadospessoais

Efectuar umareserva

Consultar asreservas pendentes

Alterar ou anularuma reserva

Enviar mensagempara o hotel

Receber mensagensdo hotel

Responder amensagem do hotel

«extend»

Consultar historial deestadias, reservas e

mensagens

Gerente

CRM4SH - Aplicação de Gestão - Administração

Registar e actualizarcaracterísticas gerais da

empresa

Registar e actualizarserviços oferecidos e

preços

Registar empregadoscom acesso ao sistema

Configuração

Registar eactualizar quartos

Estatísticas

Obter estatística detaxa de ocupação ao longo do

tempo

Obter estatística deevolução da facturação ao longo

do tempo

Obter estatística dedistribuição das vendas por

nacionalidade

Obter estatística declientes com maior

facturação

diagramas de casos de

utilização (com pacotes de

2º nível)



CRM4SH - Aplicação de Gestão - Recepção (1)

Gerente

Recepcionista

Registar novocliente

Alterar dados decliente

Gerente ou Recepcionista

Registo de Clientes

Registar reservade cliente

Alterar ou anularreserva

Reservas

Estadias

Registar entradade cliente

Registar entrada decliente sem reserva

Registar entrada decliente com reserva

Alterar data desaída prevista

Efectuar mudançade quarto

Registar saída decliente Emitir factura

«include»

CRM4SH - Aplicação de Gestão - Recepção (2)

Gerente ou Recepcionista

Gerente

Recepcionista

Consulta de ocupação

Consultar mapa deocupação

Consulta de informação de clientes

Consultar ficha ehistorial de cliente

Mensagens e Contactos

Receber mensagensde clientes

Enviar mensagempara cliente

Responder amensagem de cliente

«extend»

Registar outroscontactos com clientes

generalização


Forma do modelo de casos de utilização (3) Visão geral (cont.)

•Opcionalmente, modelar através de um ou mais diagramas de actividades o encadeamento de casos de utilização (i.e., modelar workflows ou processos de negócio)

- casos de utilização aparecem como actividades no diagrama de actividades

- se tiver sido construído anteriormente um modelo de processos de negócio, isto já foi feito


RevisoresPC CharirAutor-submissor

Submete Artigo

Atribui revisores a artigo

Revêm artigo

Decide aceitação ou rejeição

Sumbete versão final

[artigo aceite]

[artigo rejeitado]

a1 : Artigo r : RevisorArtigo1..*

notação não standard tipo“assembly line diagram”

Modelação do processo de submissão de um artigo desde a submissão até àrejeição ou submissão de versão final, por diagrama de actividades em UML

Exemplo: Sistema de Gestão de Conferências (1)

objectos de classes do modelo de domínio (ver adiante)

fluxo de objectos

fluxo de controlo

passos são execuções de casos de utilização!

actor


Exemplo: Sistema de Gestão de Conferências (2)

Revisor nRevisor 1

...Revê artigo Revê artigo

Decomposição da actividade "Revêm artigo"

barra de sincronização(inicia ou termina execução em paralelo)


Exemplo: Sistema de Gestão de Cuidados de Saúde

Médico

FuncionárioAdministrativo

Marcar Consulta

Admitir Doente

Observar

Doente

Prescrever Terapêutic

a

Carimbar Prescrição

Consulta externa: do pedido até à efectivaçãoManua

lEPRactor

internoSIIMS

Prescrição

SIIMS

Médico

Func. Admin.

EPR

Registar Dados Clínicos

Prescrever Terapêutic

a

Marcar Consulta

Admitir Doente

sistema ou sub-sistema

processo de negóciomodelado por diagrama de actividadessistema

ou sub-sistema

Registar Dados

Clínicos


Forma do modelo de casos de utilização (4) Actores

• Breve descrição de cada actor

Casos de Utilização• Descrição mais ou menos detalhada de cada caso de

utilização - ver a seguir


Descrição de cada caso de utilização Identificação e utilidade

• Nome e descrição sumária tornando evidente objectivo/utilidade

Features e restrições (Opcional)• Lista de requisitos internos ao caso de utilização

Pré-condições e pós-condições (Opcional)• Condições sobre inputs, outputs, estado inicial e estado final do sistema

(com base em modelo de estado definido no modelo de domínio – ver adiante)

• Opcionalmente, formalizar em OCL (a tratar mais tarde)

Interface e sequência de funcionamento• Mostrar sequências normais e excepcionais por diagramas de sequência• Mostrar todas as sequências possíveis por um diagrama de actividades• Opcionalmente, mostrar diagrama de navegação (diagrama de estados

com estados da interface) e esboços de interface (um esboço por estado)

Fontes e referências, classes participantes (do modelo de domínio), actores participantes, atributos (prioridade, dificuldade, ...)

Implementação – claramente fora do âmbito desta fase


Exemplo: Sistema de Gestão de Hotéis

: CRM4SH::Cliente : CRM4SH::Recepcionista

CRM4SH

Pede alojamento indicando nº de pessoas, serviço e data de saída

Introduz nº de pessoas, serviço e data de saída

Mostra lista de quartos disponíveis e preço

Informa quartos dsponíveis e preço

Confirma pedido e escolhe quarto(s)

Pede documento de identificação e cartão de crédito

Faculta documento de identificação e cartão de crédito

Regista dados de identificação do cliente

Entrega chave e cartão de estadia

Devolve documento de identificação e cartão de crédito

Imprime cartão da estadia

Selecciona quarto(s) da lista

Regista dados do cartão de crédito do cliente

Sist. Externo de Valid. de Cartões

Valida cartão

Cartão Ok

diagrama de sequência, mostrando sequência normal de funcionamento do caso de utilização "Registar entrada de cliente sem reserva"

objectos

mensagens


Exemplo: Sistema de Gestão de HotéisSist. Ext. de

Valid. deCartões

CRM4SHRecepcionistaCliente

Pede alojam. p/ nºpess. e dt.saída Introduz dados do pedido

Mostra lista de quartos disponíveis e preçoInforma quartos disponíveis e preço

Escolhe quarto(s)

Pede identificação e cartão de crédito

Selecciona quarto(s) da lista

Faculta doc. ident. e cartão crédito

Memoriza informação

Regista dados de identificação do cliente

Memoriza informação

Regista dados do cartão de crédito do cliente

Solicita validação do cartão Valida cartão

Regista estadia na base de dados

[cartão ok]

Verifica disponibilidade

[disponível]

Informa cliente[indisponível]

Cancela e informa utilizador[cartão inválido]

Informa cliente

[não aceita]

Cancela operação[aceita]

Imprime cartão da estadiaDevolve documento de identificaçãoRecolhe documento de identificação

Entrega chaveRecolhe chave

Entrega cartão da estadiaRecolhe cartão da estadia

Devolve cartão de créditoRecolhe cartão de crédito

diagrama de actividades, mostrando todas as sequências possíveis de funcionamento do caso de utilização "Registar entrada de cliente sem reserva"


Exemplo: Sistema de Gestão de Conferências

seleccionar opção "Atribuir revisores a artigos" Terminar

Atribuir Revisores a Artigos

artigo nº de revisores

terminar

titulo1 0titulo 2 1

Terminar

Atribuir Revisores a Artigo

artigo

seleccionar artigo

título:autores: autor1, autor2, ...resumo:

PDF

nome nº art.

revisor 1 3revisor 2 1

excluir

excluir

excluir

revisores atribuídos

terminar

excluir

nome nº art.

revisor 3 3revisor 4 0

atribuiratribuir

atribuir

revisores disponíveis

atribuirFechar

Dados de Revisor

nome:instituição:e-mail:áreas de interesse:artigos que revê: artigo1, ...

seleccionar revisor

fechar

evento (acção do utilizador)

estado da interface

Diagrama de navegação do caso de utilização "Atribuir Revisores a Artigos" (diagrama de estados em UML, em que estados são estados de interface):


Modelo de (objectos de) domínio (1) Objectivos

• organizar o vocabulário do domínio do problema (utilizado na descrição dos casos de utilização)

- organizar e relacionar termos que estão definidos num glossário ou num dicionário de dados

• capturar os requisitos de informação - que informação é mantida no sistema e trocada com o

ambiente

• especificar as transacções do negócio (por operações)

• três tipos de classes- classes que modelam o estado interno persistente e partilhado

do sistema, como atributos de entidades (e eventos) do negócio e respectivas ligações – são as classes mais importantes

- classes que modelam a estrutura de documentos trocados entre o sistema e o seu ambiente

- classes que modelam tipos de dados (usados nos atributos e operações das classes anteriores)


Modelo de (objectos de) domínio (2) Forma

•Visão geral- Diagrama de classes- Descrição textual que passa superficialmente pelas

classes mais importantes



generalização

classe-associação (para indicar atributos)

agregação

classe com atributos

nota

diagrama de classes

associação

nomeendereçotelefonecategoriae-mail/capacidade

Hotel

número de cliente {I}nomenacionalidadedata de nascimentomoradatelefonenúmero do bilhete de identidade ou passaporte {I2}data do bilhete de identidade ou passaportee-mail

Cliente

número da reserva {I}data da reservanúmero de pessoasdata de entrada previstadata de saída previstanúmero do cartão de créditotitular do cartão de créditodata de expiração do cartão de créditoestado: (activa, anulada, efectivada, cliente faltou)

Reserva

número da estadia {I}número de pessoasdata de entradadata de saídanúmero do cartão de créditotitular do cartão de créditodata de expiração do cartão de crédito

Estadia

0..10..1

1

*

1

*

número {I}capacidade

Quarto

nome {I}

Serviço

1

*

1 serviços1..*

1

quartos*clientes *

1

data de início {I}data de fimnúmero de pessoas {I}preço

Preço Serviço

serviço {I}

1

preços1..*

login {I}passwordnomefunção

Empregado

1

empregados*

1

*

número {I}data/valor

Factura

1

0..1

1

*

/

Mensagem por e-mail

data-horamodo de contactoiniciativa do contactodescrição

Contacto com Clientecontacto anterior

0..1

contacto seguinte*

0..1

*

1

*

0..1

*

0..1

*

1

data de entradadata de saídanúmero de pessoas

Estadia Quarto

*

1..*

Permite manterinformação demudanças dequarto e indicara distribuição depessoas pelosquartos.

(versão corrigida para ficar consistente com OCL)


Modelo de (objectos de) domínio (3)

Forma (cont.)• Descrição de cada classe

- Significado- Descrição de atributos - Definição de restrições

- Informalmente- Formalmente, como invariantes em OCL (a ver mais tarde)

- Descrição de operações (quando definidas)- Sintaxe- Semântica

• Informalmente• Formalmente, com pré-condições e pós-condições em OCL (a ver mais

tarde)- (Opcional) Ciclo de vida dos objectos da classe

(diagrama de estados)- Estados devem corresponder a condições nos valores de

atributos e ligações- Nesta fase, eventos devem corresponder a casos de

utilização, podendo ter parâmetros


Activa

registo de reserva

Anulada

Cliente faltou

Efectivada

eliminação da informação

anulação de reservaregisto de entrada com reserva

passagem da data de entrada prevista


ciclo de vida de uma reserva (diagrama de estados) estado

estado composto

subestado

evento (corresponde a execução de caso de utilização)

transição

evento temporal












O que é OCL? OCL = Object Constraint Language

Faz parte de UML

Linguagem textual para formalizar invariantes, pré-condições e pós-condições por intermédio de expressões booleanas sem efeitos laterais

• Expressões podem invocar métodos que consultam o estado de objectos (query methods), mas não métodos que alteram o estado de objectos ou criam ou eliminam objectos

Baseada em conceitos matemáticos (conjuntos, sequências, lógica matemática, etc.)

Versão corrente: 1.5

Versão em preparação: 2.0


Especificação de invariantes em OCL Invariantes são restrições a que devem obedecer os

estados válidos Definidos em OCL usando palava-chave inv Em OCL, invariantes são sempre definidos no contexto de

uma classe (ou objecto de classe) Tipos de invariantes comuns:

• restrição ao domínio (ou conjunto de valores possíveis) de um atributo

• chaves de uma classe - atributo ou conjunto de atributos de uma classe que não pode tomar o mesmo valor (ou conjunto de valores) em dois objectos diferentes da classe

• restrições relacionadas com ciclos nas associações• restrições relacionadas com datas e horas• restrições que definem a fórmula de derivação de elementos

derivados (replicados ou calculados)• regras de existência – indicam que certos objectos devem existir

quando outros objectos existem


Exemplo: Sistema de Gestão de HotéisRestrições a domínios de atributos (1) R1) Em "Preço Serviço", o número de pessoas tem de ser maior que

0

context Preço_Serviço inv: número_de_pessoas > 0

R2) Em "Estadia", o número de pessoas tem de ser maior que 0

context Estadia inv: número_de_pessoas > 0

R3) Em "Reserva", o número de pessoas tem de ser maior que 0

context Reserva inv: número_de_pessoas > 0

R4) Em "Estadia_Quarto", o número de pessoas tem de ser maior que 0

context Estadia_Quarto inv: número_de_pessoas > 0


Exemplo: Sistema de Gestão de HotéisRestrições a domínios de atributos (2)

R5) Em "Quarto", a capacidade tem de ser maior que 0

context Quarto inv: capacidade > 0

R6) Em "Preço_Serviço", o preço tem de ser maior que 0

context Preço_Serviço inv: preço > 0


Elementos de OCL

Formas equivalentes:

context Reserva inv: número_de_pessoas > 0

context Reserva inv: self.número_de_pessoas > 0

context r : Reserva inv: r.número_de_pessoas > 0

Pode-se dar um nome ao invariante:

context Reserva inv NumPesResPos: número_de_pessoas > 0


Exemplo: Sistema de Gestão de HotéisChaves simples (1)

R7) Não podem existir dois clientes com o mesmo número, isto é, o número de cliente é chave

context Cliente inv R7: Cliente.allInstances->isUnique(número_de_cliente)

R7') (Equivalente a anterior, porque só há 1 hotel) Um hotel não pode ter dois clientes com o mesmo número

context Hotel inv R7b: clientes->isUnique(número_de_cliente)

Nota: Sempre que possível é de evitar usar classe.allInstances, pois é fácil implementar numa base de dados mas é difícil implementar em objectos em memória (em memória prefere-se partir de um objecto raiz).


Elementos de OCLColecções Cliente.allInstances dá o conjunto (Set) de todas as instâncias

existentes da classe Cliente O operador "->" toma o lado esquerdo como colecção e aplica-lhe a

operação indicada no lado direito Colecções em OCL podem ser dos seguintes tipos

• Set – conjunto de elementos distintos• Bag – conjunto admitindo elementos repetidos• Sequence – sequência de elementos admitindo repetição • OrderedSet (só versão 2.0) – conjunto ordenado de elementos distintos

Uma colecção OCL contém objectos (instâncias de classes) ou valores de tipos primitivos (Integer, Real, Boolean ou String)

• Classes são tipos-referência (reference types)- variáveis contêm referências para objectos; comparação e atribuição

de referências• Tipos primitivos, colecções e tuplos (ver adiante) são tipos-valor (value

types)- variáveis contêm os próprios valores; comparação e atribuição de

valores- equivalem a tipos-referência em que não se podem criar duas

instâncias (objectos) com o mesmo conteúdo e o conteúdo de uma instância é imutável


Elementos de OCLOperações com colecções (1) collection->exists(expressãoBooleana) – dá true se a expressão

for verdadeira para pelo menos um elemento da colecção

x collection : expressãoBooleana(x)

collection->forAll(expressãoBooleana) – dá true se a expressão for verdadeira para todos os elementos da colecção

x collection : expressãoBooleana(x)

collection->isUnique(expressão) – dá true não existirem dois elementos da colecção com o mesmo valor da expressão

x, y collection : x y expressão(x) expressão(y)

collection->notEmpty()

collection->select(expressãoBooleana) – selecciona os elementos da colecção para os quais a expressão é verdadeira

• { x collection | expressãoBooleana(x) } - (tb. com sequências)


Elementos de OCLOperações com colecções (2)

collection->collect(expressão) – produz uma nova colecção formada pelos valores da expressão indicada sobre os elementos da primeira colecção

collection->sum() – soma valores de uma colecção de inteiros ou reais

collection->including(elem) – dá nova colecção incluindo o elemento indicado

collection->excluding(elem) – dá nova colecção excluindo o elemento indicado

collection->iterate(iterador; DeclaraçãoEInicializaçãoAcumulador | proximoValorAcumulador) – dá o valor final do acumulador depois de iterar sobre todos os elementos da colecção

collection->any(expressãoBooleana) – dá um elemento qualquer da colecção que verifica a expressão booleana indicada


Elementos de OCLNavegação através de associações e classes-associações

Estadia Quarto

Estadia_Quarto

quartos**

No contexto de uma instância de Estadia:• quartos – conjunto de instâncias correspondentes da classe Quarto (usa-se o rolename), do

tipo Set(Quarto)• estadia_Quarto – conjunto de instâncias correspondentes da classe-associação Estadia_Quarto

(usa-se o nome da classe-associação com 1ª letra em minúscula), do tipo Set(Estadia_Quarto)

No contexto de uma instância de Quarto:• estadia – conjunto de instâncias correspondentes da classe Estadia (como não existe

rolename, usa-se o nome da classe com 1ª letra em minúscula), do tipo Set(Estadia)• estadia_Quarto – conjunto de instâncias correspondentes da classe-associação Estadia_Quarto

(usa-se o nome da classe-associação com 1ª letra em minúscula), do tipo Set(Estadia_Quarto)

No contexto de uma instância de Estadia_Quarto:• quartos – instância correspondente da classe Quarto (usa-se o rolename), do tipo Quarto • estadia – instância correspondente da classe Estadia (como não existe rolename, usa-se o

nome da classe com 1ª letra em minúscula), do tipo Estadia

quartos: Set(Quarto)estadia_Quarto: Set(Estadia_Quarto)

estadia: Set(Estadia)estadia_Quarto: Set(Estadia_Quarto)

quartos: Quartoestadia: Estadia

versão 4.0


Elementos de OCLNavegação através de associações qualificadas

Hotel Pessoacliente0..1

No contexto de uma instância de Hotel:• cliente – conjunto de instâncias correspondentes da classe Cliente, do

tipo Set(Pessoa)• cliente[i] – instância da classe Pessoa correspondente a númeroCliente = i

No contexto de uma instância de Pessoa:• hotel – conjunto de instâncias correspondentes da classe Hotel, do

tipo Set(Hotel)

Dado um hotel, como obter o seu conjunto de números de clientes (instâncias do qualificador)??

Dada uma pessoa, como obter o seu conjunto de pares hotel +número de cliente??

cliente : Set(Pessoa)cliente[i]: Pessoa

hotel: Set(Hotel)

númeroCliente1..*

versão 4.0


Elementos de OCLNavegação para classe-associação em associação recursiva

Empregado

Avaliação*

No contexto de uma instância de Empregado:• chefes – conjunto de chefes correspondentes (instâncias de Empregado)

• subordinados – conjunto de subordinados correspondentes (instâncias de Empregado)

• avaliação[chefes] – conjunto de instâncias correspondentes da classe-associação Avaliação quando se navega do empregado para os seus chefes (permite aceder às avaliações que foram atribuídas ao empregado pelos seus chefes)

• avaliação[subordinados] - conjunto de instâncias correspondentes da classe-associação Avaliação quando se navega do empregado para os seus subordinados (permite aceder às avaliações que o empregado atribuiu aos seus subordinados)

chefes

subordinados * avaliação guarda avaliação atribuída pelo chefe ao subordinado

versão 4.0


Exemplo: Sistema de Gestão de HotéisChaves simples (2)

R8) (Chave alternativa) Não podem existir dois clientes com o mesmo número de bilhete de identidade ou passaporte (este atributo pode ser visto como uma combinação de tipo de documento + número de documento)

context Cliente inv: Cliente.allInstances->isUnique( número_do_bilhete_de_identidade_ou_passaporte)

R9) Não podem existir duas reservas com o mesmo número

context Reserva inv: Reserva.allInstances->isUnique(número_da_reserva)

R10) Não podem existir duas estadias com o mesmo número

context Estadia inv: Estadia.allInstances->isUnique(número_da_estadia)


Exemplo: Sistema de Gestão de HotéisChaves simples (3) R11) Não podem existir dois quartos com o mesmo número

context Quarto inv: Quarto.allInstances->isUnique(número)

R12) Não podem existir dois empregados com o mesmo login

context Empregado inv: Empregado.allInstances->isUnique(login)

R13) Não podem existir duas facturas com o mesmo número

context Factura inv: Factura.allInstances->isUnique(número)

R14) Não podem existir dois serviços com o mesmo nome

context Serviço inv: Serviço.allInstances->isUnique(nome)


Exemplo: Sistema de Gestão de HotéisChaves compostas R15) Em "Preço Serviço", não podem existir duas ocorrências para

a mesma combinação de serviço, data de início e número de pessoas

Em OCL 2.0 (em preparação), existe o conceito de tuplo (conjunto de componentes com nome e valor), pelo que se poderá escrever:

context Preço_Serviço inv: Preço_Serviço.allInstances->isUnique(p : Preço_Serviço | Tuple{serviço : Serviço = p.serviço, data_de_início: Date = p.data_de_início, número_de_pessoas : Integer = p.número_de_pessoas} )

Ou omitindo os tipos do iterador e dos componentes dos tuplos:

context Preço_Serviço inv: Preço_Serviço.allInstances->isUnique(p | Tuple{serviço = p.serviço, data_de_início = p.data_de_início, número_de_pessoas = p.número_de_pessoas} )

variável/iterador (para desambiguar)

separador entre iterador e expressão


Exemplo: Sistema de Gestão de HotéisChaves em classes derivadas R16) Em "Preço Serviço", não podem existir duas ocorrências

para a mesma data, número de pessoas e serviço (chave em classe derivada resultante de desdobrar "Preço Serviço" por datas)

context Preço_Serviço inv: not Preço_Serviço.allInstances->exists(p1, p2 | p1 <> p2 and p1.serviço = p2.serviço and DateInterval.overlap(p1.data_de_início, p1.data_de_fim, p2.data_de_início, p2.data_de_fim, false) and p1.número_de_pessoas = p2.número_de_pessoas)

Notas: 1) Esta restrição implica a restrição anterior (R15)2) Uma vez que o standard não inclui a definição do tipo Date, pressupõe-se definição apropriada dos tipos Date e DateInterval (ver adiante)


Exemplo: Sistema de Gestão de HotéisRestrições relacionadas com ciclos (1)

R17) A reserva a que se refere uma estadia tem de ser do mesmo cliente que a estadia

context Estadia inv: reserva->notEmpty() implies reserva.cliente = cliente

Nota: "reserva" designa o objecto correspondente pela associação c/"Reserva", cuja multiplicidade é 0..1, pelo que é necessário fazer o teste

R18) A reserva a que se refere um contacto tem de ser do mesmo cliente que o contacto

context Contacto inv: reserva->notEmpty() implies reserva.cliente = cliente


Exemplo: Sistema de Gestão de HotéisRestrições relacionadas com ciclos (2)

R19) A estadia a que se refere um contacto tem de ser do mesmo cliente que o contacto.

context Contacto inv: estadia->notEmpty() implies estadia.cliente = cliente

R20) O contacto anterior a que se refere um contacto tem de ser do mesmo cliente que o contacto actual.

context Contacto inv: contacto_anterior->notEmpty() implies contacto_anterior.cliente = cliente

Nota: ver mais em elementos derivados


Exemplo: Sistema de Gestão de HotéisRestrições relacionadas com datas (1) R21) Numa reserva, a data de saída prevista tem de ser posterior

à data de entrada prevista

context Reserva inv: data_de_saída_prevista.isAfter(data_de_entrada_prevista)

R22) Numa reserva, a data de entrada prevista não pode ser anterior à data da reserva

context Reserva inv: not data_da_reserva.isBefore(data_de_entrada_prevista)

R23) Numa estadia, a data de saída tem de ser posterior à data de entrada

context Estadia inv: data_de_saída.isAfter(data_de_entrada)


Exemplo: Sistema de Gestão de HotéisRestrições relacionadas com datas (2) R24) Numa estadia, a data de expiração do cartão de crédito tem

de ser posterior à data de saída

context Estadia inv R24: data_de_expiração_do_cartão_de_crédito.isAfter(data_de_saída)

R25) Em "Estadia Quarto", a data da saída tem de ser posterior à data de entrada

context Estadia_Quarto inv R25: data_de_saída.isAfter(data_de_entrada)

R26) O intervalo de datas de uma ocorrência de "Estadia Quarto" (classe-associação), tem de estar contido no intervalo de datas da estadia correspondente

context Estadia_Quarto inv R26: DateInterval.contains(estadia.data_de_entrada, estadia.data_de_saída, data_de_entrada, data_de_saída, true)


Exemplo: Sistema de Gestão de HotéisRestrições relacionadas com datas (3) R27) Na relação entre contactos, a data-hora do contacto

anterior tem de ser anterior à data-hora do contacto seguinte

context Contacto inv R27: contacto_anterior->notEmpty() implies contacto_anterior.data_hora.isBefore(data_hora)

Nota: Pressupõe definição de tipo DateTime com operações apropriadas


Exemplo: Sistema de Gestão de HotéisRegras de existência R28) Têm de estar definidos preços para se aceitarem estadias ou

reservas

context e: Estadia inv R28a: e.data_de_entrada.getDatesUntil(e.data_de_saída, true) ->forAll(d | e.serviço.preços ->exists( p | p.número_de_pessoas = e.número_de_pessoas and p.data_de_início.containsUntil(p.data_de_fim, d, true))

context r: Reserva inv 28b: r.data_de_entrada_prevista. getDatesUntil(r.data_de_saída_prevista, true) ->forAll(d | r.serviço.preços ->exists( p | p.número_de_pessoas = r.número_de_pessoas and p.data_de_início.containsUntil(p.data_de_fim, d, true) )

Notas: na realidade, seria mais correcto definir em Hotel atributos com número máximo de pessoas por estadia/reserva e gama de datas com preços definidos (data inicial e final), e obrigar depois a estarem definidos preços para todos os serviços, nº de pessoas e datas nas gamas definidas


Exemplo: Sistema de Gestão de HotéisConsistência de preços R29) Aumentando o número de pessoas o preço (do grupo) não pode

baixar

context Preço_Serviço inv R29: Preço_Serviço.allInstances->forAll(p1, p2 | p1.serviço = p2.serviço and p1.número_de_pessoas > p2.número_de_pessoas and DateInterval.overlap(p1.data_de_início, p1.data_de_fim, p2.data_de_início, p2.data_de_fim, true) implies p1.preço >= p2.preço)

R30) Partindo um grupo o preço não pode baixar

context Preço_Serviço inv R30: Preço_Serviço.allInstances->forAll(p1, p2, p3 | p1.serviço = p2.serviço and p1.serviço = p3.serviço and DateInterval.overlap(p1.data_de_início, p1.data_de_fim, p2.data_de_início, p2.data_de_fim, true) and DateInterval.overlap(p1.data_de_início, p1.data_de_fim, p3.data_de_início, p3.data_de_fim, true) and DateInterval.overlap(p2.data_de_início, p2.data_de_fim, p3.data_de_início, p3.data_de_fim, true) and p1.número_de_pessoas = (p2.número_de_pessoas + p3.número_de_pessoas) implies p1.preço <= p2.preço + p3.preço)


Exemplo: Sistema de Gestão de HotéisConsistência de estados R31) Uma reserva no estado "efectivada" é uma reserva com

uma estadia associada

context Reserva inv R31: (estado = 'efectivada') = estadia->notEmpty()

R32) Assim que se ultrapassa a data de entrada prevista de uma reserva sem que o cliente compareça, uma reserva que não foi cancelada passa ao estado "cliente faltou"

context Reserva inv R32: (Date.curDate.isAfter(data_de_entrada_prevista) and estadia->isEmpty() and estado <> 'anulada') = (estado = 'cliente faltou')


Exemplo: Sistema de Gestão de HotéisRestrições relativas à ocupação do hotel (1) R33) O mesmo quarto não pode estar ocupado duas vezes na

mesma data (isto é, não pode ter duas ocorrências de "Estadia Quarto" na mesma data)

context Quarto inv R33: estadia_Quarto->forAll( e1, e2 | e1 <> e2 implies DateInterval.disjoint(e1.data_de_entrada, e1.data_de_saída, e2.data_de_entrada, e2.data_de_saída, true))

R34) O número de pessoas colocadas num quarto tem de estar compreendido entre 1 e a capacidade do quarto.

context Estadia_Quarto inv R34: número_de_pessoas >= 1 and número_de_pessoas <= quarto.capacidade


Exemplo: Sistema de Gestão de HotéisRestrições relativas à ocupação do hotel (2)

R35) Para qualquer data e estadia, a soma dos números de pessoas indicados em "Estadia Quarto" deve ser igual ao número de pessoas indicado em "Estadia"

context e: Estadia inv R35: e.data_de_entrada.getDatesUntil(e.data_de_saída, true) ->forAll(d | e.número_de_pessoas = e.estadia_quarto ->select(q | q.data_de_entrada.containsUntil(q.data_de_saída, d, true)) ->collect(número_de_pessoas) ->sum() )


Exemplo: Sistema de Gestão de HotéisRestrições relativas à ocupação do hotel (3)

R36) Deve ser possível satisfazer todas as reservas activas. context Reservadef: arranjaQuartos( gruposPorColocar: Bag(Tuple(entrada: Date, saída: Date, n_pessoas: Integer)), gruposColocados : Set(Tuple(entrada: Date, saída: Date, quarto: Quarto)) ) : Boolean =( gruposPorColocar->notEmpty() implies let g = gruposPorColocar->any(true) in Quarto.allInstances->exists (q | gruposColocados->forall(gc | gc.quarto = q implies DateInterval.disjoint(gc.entrada, gc.saída, g.entrada, g.saída, true)) and arranjaQuartos( if q.capacidade >= g.n_pessoas then gruposPorColocar->excluding(g) else gruposPorColocar->excluding(g) ->including(Tuple{entrada = g.entrada, saída = g.saída, n_pessoas = g.n_pessoas – q.capacidade}) endif, gruposColocados->including(Tuple{entrada = g.entrada, saída = g.saída, quarto = q}))) )inv R36: arranjaQuartos(Reserva.allInstances->select(estado = 'activa')->collect( r | Tuple{entrada = r.data_de_entrada, saída = r.data_de_saída, n_pessoas = r.número_de_pessoas}), Estadia_Quarto.allInstances->collect( eq | Tuple{entrada = eq.data_de_entrada, saída = eq.data_de_saída, quarto = eq.quarto}))

modificado versão 3.0


Exemplo: Sistema de Gestão de HotéisRestrições relativas a elementos derivados

R37) A capacidade do hotel é a soma das capacidades dos seus quartos (caso de dado calculado)

Context Hotel inv R37: capacidade = quartos->select(capacidade)->sum()

R38) O cliente da factura é o cliente da estadia a que se refere a factura (caso de dado replicado)

Context Factura inv R38: cliente = estadia.cliente

R39) O valor da factura é calculado em função dos preços tabelados

Context Factura inv R39: valor = estadia.serviço.preços ->select(p | p.número_de_pessoas = estadia.número_de_pessoas) ->collect(p | p.preço * Integer.max(0, 1+Date.difference( Date.min(estadia.data_de_fim, p.data_de_fim), Date.max(estadia.data_de_início, p.data_de_início))) ->sum()


Exemplo: Sistema de Gestão de HotéisRestrições relativas a elementos derivados (OCL 2.0)Na versão 2.0 será possível escrever: R37') A capacidade do hotel é a soma das capacidades dos seus

quartos

Context Hotel::capacidade : Integer derive: quartos->select(capacidade)->sum()

R38) O cliente da factura é o cliente da estadia a que se refere a factura

Context Factura::cliente : Cliente derive: estadia.cliente

R39) idem


Exemplo: Sistema de Gestão de HotéisDefinição dos tipos Date, DateTime e DateInterval (1)

Date

toInteger(): Integer isAfter(d2: Date) : Boolean isBefore(d2: Date) : Boolean max(d1: Date, d2: Date) : Date min(d1: Date, d2: Date) : Date difference(d1: Date, d2: Date) : Integer

DateTime

isAfter(d2: DateTime) : BooleanisBefore(d2: DateTime) : Boolean

curDate : Date

DateInterval

disjoint(left1: Date, right1: Date, left2: Date, right2: Date, openRight: Boolean ) : Booleanoverlap(left1: Date, right1: Date, left2: Date, right2: Date, openRight: Boolean ) : Booleancontains(left1: Date, right1: Date, left2: Date, right2: Date, openRight: Boolean ) : Boolean(...) Apenas foram indicados métodos

que não alteram estado, e que por isso podem ser usados em expressões OCL


Exemplo: Sistema de Gestão de HotéisDefinição dos tipos Date, DateTime e DateInterval (2)

Definição de operações auxiliares em OCL (OclHelper)

context Date-- obtém conjunto de datas representadas por inteiros desde self até uma-- outra data (right), incluída ou excluídadef: getDatesUntil(right: Date, openRight: Boolean) : Set(Integer) = if openRight then Sequence{self.asInteger() .. (right.asInteger()-1)}->asSet() else Sequence{self.asInteger() .. right.asInteger()}->asSet() endif

-- verifica se o intervalo que vai desta data (self) até outra data (right), -- incluída ou excluída, contém uma terceira data representada por inteirodef: containsUntil(right: Date, data: Integer, openRight: Boolean ) : Boolean = data >= self.asInteger() and data <= (if openRight then right.asInteger()-1 else right.asInteger() endif)

Nota: como não se pode dizer que são static, foram definidas em Date em vez de em DateInterval


Especificação da semântica de operações em OCL Nos diagramas de classes apenas se indica a sintaxe ou

assinatura das operações A semântica das operações pode ser especificada por pré-

condições e pós-condições em OCL A pré-condição é uma condição booleana nos argumentos de

chamada e estado inicial do(s) objecto(s) a que deve obedecer uma chamada válida

• Pré-condição é indicada a seguir a "pre:"

A pós-condição é uma condição booleana nos argumentos de chamada, valor retornado, estado inicial do(s) objecto(s), e estado final do(s) objecto(s) que se deve verificar no final da execução da operação, supondo que a pré-condição se verifica

• Pós-condição é indicada a seguir a "post:"• Indica o efeito que a operação deve produzir, sem indicar o algoritmo• Estado inicial de uma propriedade de um objecto é acedido com o

sufixo "@pre" (ver a seguir)• Valor retornado pela operação é acedido com "result"


Acesso a valores antigos em pós-condições (1) propriedade@pre – valor antigo da propriedade (no início

da execução da operação a que se refere a pós-condição)

Se não se usar "@pre", estamos a aceder ao novo valor da propriedade, i.e., ao valor no fim da execução da operação

São consideradas propriedades:• atributos• extremos de associações• operações ou métodos sem efeitos laterais (só de consulta)

Estas propriedades podem estar definidas em:• classes, interfaces e tipos (interfaces e tipos são classes especiais)• associações• tipos de dados primitivos (datatypes)


Acesso a valores antigos em pós-condições (2) No caso de operações ou métodos, "@pre" é colocado

entre o nome da operação e a lista de argumentos• operação@pre(argumentos)

Quando o valor antigo de uma propriedade se refere a um objecto, é necessário voltar a usar "@pre" se quisermos aceder a valores antigos de propriedades desse objecto

• [email protected] -- takes the old value of property b of a, say x -- and then the new value of c of x.

• [email protected]@pre -- takes the old value of property b of a, say x -- and then the old value of c of x.

Não se pode aceder ao valor antigo de uma propriedade de um objecto criado no decurso da operação, nem ao novo valor antigo de uma propriedade de um objecto destruído no decurso da operação. Senão o resultado é OclUndefined


Exemplo: Sistema de Gestão de HotéisDefinição de pré e pós-condições de reserva (1)

Registo de reserva – 1ª versão, recebendo e devolvendo objectos

context Reserva::criarReserva( cliente: Cliente, serviço: Serviço, número_de_pessoas: Integer, data_de_entrada_prevista: Date, data_de_saída_prevista: Date, número_do_cartão_de_crédito: Integer, titular_do_cartão_de_crédito: String, data_de_expiração_do_cartão_de_crédito: Date): Reserva

pre: número_de_pessoas > 0 -- R3 and not data_de_entrada_prevista.isBefore(Date.curDate()) -- R32 and data_de_saída_prevista.isAfter(data_de_entrada_prevista) -- R21 and data_de_expiração_do_cartão_de_crédito.isAfter(data_de_saída_prevista) -- R24 and Hotel.temQuartos(data_de_entrada_prevista, data_de_saída_prevista, número_de_pessoas) -- R36 and serviço.temPreços(data_de_entrada_prevista, data_de_saída_prevista, número_de_pessoas) -- R28 and GestãoCartões.cartãoVálido(número_do_cartão_de_crédito, titular_do_cartão_de_crédito, data_de_expiração_do_cartão_de_crédito) -- envolve acesso a sistema externo (continua) Exercício: definir em OCL as operações

auxiliares temQuartos e temPreços (ver R36 e R28)



(continuação)post: result.oclIsNew() -- ou: Reserva.allInstances = Reserva.allInstances@pre->including(result)

-- atributos com valores dados pelos argumentos da operação and result.número_de_pessoas = número_de_pessoas and result.data_de_entrada_prevista = data_de_entrada_prevista and result.data_de_saída_prevista = data_de_saída_prevista and result.data_de_saída_prevista = data_de_saída_prevista and result.número_do_cartão_de_crédito = número_do_cartão_de_crédito and result.titular_do_cartão_de_crédito = titular_do_cartão_de_crédito and result.data_de_expiração_do_cartão_de_crédito = data_de_expiração_do_cartão_de_crédito

-- associações and result.serviço = serviço and result.cliente = cliente and result.estadia->isEmpty() and result.contacto_com_Cliente->isEmpty() -- atributos calculados and result.data_da_reserva = Date.curDate() and result.estado = 'activa' and result.número_da_reserva = 1 + Reserva.allInstances@pre-> iterate(r; maiorNum: Integer = 0 | maiorNum.max(r.número_da_reserva@pre))

Como dizer que não há mais alterações de estado além das referidas explicitamente?!

Pós-condição está escrita de forma construtiva!



Registo de reserva - 2ª versão, recebendo e devolvendo chaves de objectos

context Reserva::criarReserva( número_de_cliente: Integer, nome_do_serviço: String, número_de_pessoas: Integer, data_de_entrada_prevista: Date, data_de_saída_prevista: Date, número_do_cartão_de_crédito: Integer, titular_do_cartão_de_crédito: String, data_de_expiração_do_cartão_de_crédito: Date): Integer -- número_da_reserva

pre: Cliente.allInstances->exists(c| c.número_de_cliente = número_de_cliente) -- integridade referencial and Serviço.allInstances->exists(s| s.nome = nome_do_serviço) -- integridade referencial and ... (o resto como anteriormente)

post: let cliente : Cliente = Cliente.allInstances@pre-> select(c| c.número_de_cliente@pre = número_de_cliente)->any(true), serviço : Serviço = Serviço.allInstances@pre-> select(s| s.nome@pre = nome_do_serviço)->any(true), novas_reservas : Set(Reserva) = Reserva.allInstances - Reserva.allInstances@pre in novas_reservas->size() = 1 and let reserva : Reserva = novas_reservas->any(true) in result = reserva.número_da_reserva and ... (o resto como anteriormente, com "result" substituído por "reserva")


Exemplo: Sistema de Gestão de HotéisDefinição de pré e pós-condições de check-in (1)

Check-in com reserva prévia – versão em que quartos são atribuídos automaticamente

context Estadia::checkInComReserva(reserva: Reserva): Estadia

pre: reserva.estado = 'activa' and reserva.data_de_entrada_prevista = Date.curDate()

post: result.oclIsNew() and result.número_de_pessoas = reserva.número_de_pessoas@pre and result.data_de_entrada = reserva.data_de_entrada_prevista@pre and result.data_de_saída = reserva.data_de_saída_prevista@pre and result.número_do_cartão_de_crédito = reserva.número_do_cartão_de_crédito@pre and result.titular_do_cartão_de_crédito = reserva.titular_do_cartão_de_crédito@pre and result.data_de_expiração_do_cartão_de_crédito = reserva.data_de_expiração_do_cartão_de_crédito@pre and result.número_da_estadia = 1 + Estadia.allInstances@pre-> iterate(r; maiorNum: Integer = 0 | maiorNum.max(r.número_da_estadia@pre)) and result.cliente = reserva.cliente@pre and result.serviço = reserva.serviço@pre and result.reserva = reserva and result.contacto_com_Cliente->isEmpty() and result.factura->isEmpty() (continua)

Exercício: escrever pré e pós-condição de check-out


Exemplo: Sistema de Gestão de HotéisDefinição de pré e pós-condições de check-in (2)

(continuação) -- actualização do estado da reserva and reserva.estadia = result and reserva.estado = 'efectivada'

-- Condições a que tem de obedecer a atribuição automática de quartos (sem mudanças de quartos):

-- selecção de quartos (já optimizada) and reserva.escolhasQuartosPossiveis@pre->includes(result.estadia_Quarto->collect(quarto) ) -- ver definição de escolhasQuartosPossiveis a seguir

-- definição de datas de estadia em cada quarto (garantindo R26) and result.estadia_Quarto->forall(eq | eq.data_de_entrada = result.data_de_entrada and eq.data_de_saída = result.data_de_saída)

-- escolha de número de pessoas em cada quarto (garantindo R34 e R35) and result.estadia_Quarto->forall(eq | eq.número_de_pessoas >= 1 and eq.número_de_pessoas <= quarto.capacidade) and result.estadia_Quarto->collect(eq | eq.número_de_pessoas)->sum() = result.número_de_pessoasNeste caso, a pós-condição não fixa completamente o estado final (nomeadamente o conjunto de quartos escolhidos e o número de pessoas em cada quarto), apenas fixa as condições a obedecer na produção do estado final.


Exemplo: Sistema de Gestão de HotéisDefinição de operação auxiliar para escolher quartos (1) context reserva: Reserva

-- Obtém o conjunto de escolhas possíveis de quartos para uma reserva.-- Cada escolha é um conjunto com um ou mais quartos.-- As escolhas são efectuadas por forma a não inviabilizar a satisfação das outras reservas.-- São excluídas escolhas de quartos nitidamente inferiores em relação ao objectivo de maximizar-- a taxa de ocupação do hotel (aceitar mas estadias/reservas posteriores). def: escolhasQuartosPossíveis : Set(Set(Quarto)) = let -- obtém o conjunto de quartos que não têm estadias em curso no período da reserva quartosLivres : Set(Quarto) = Quarto.allInstances->select(estadia_Quarto->forall(eq | DateInterval.disjoint(eq.data_de_entrada, eq.data_de_saída, reserva.data_de_entrada, reserva.data_de_saída, true))), -- dado um conjunto de quartos livres, obtém (recursivamente) o conjunto dos seus subconjuntos -- não vazios, excluindo subconjuntos com quartos em excesso para satisfazer a reserva subconjuntosQuartos(quartos : Set(Quarto)): Set(Set(Quarto)) = if quartos->isEmpty() then Set{} else let este : Quarto = quartos->any(true), semEste : Set(Set(Quarto)) = subconjuntosQuartos(quartos->excluding(este)), comEste : Set(Set(Quarto)) = Set{Set{este}}->union(semEste-> ->select(qq | qq->collect(capacidade)->sum() < reserva.número_de_pessoas) ->collectNested(qq | qq->including(este)) in semEste->union(comEste) endif, (continua)

só versão 2.0; collect não serve pois não permite criar conjuntos de conjuntos (aplana tudo num só conjunto)


Exemplo: Sistema de Gestão de HotéisDefinição de operação auxiliar para escolher quartos (2)

(continuação) -- verifica se uma escolha de quartos livres é válida, isto é, se o número de quartos é suficiente -- para satisfazer esta reserva e se não inviabiliza a satisfação das restantes reservas (usando -- a operação auxiliar arranjaQuartos definida a propósito da restrição R36) escolhaVálida(quartos: Set(Quarto)) : Boolean = quartos->select(capacidade)->sum() >= reserva.número_de_pessoas and arranjaQuartos( Reserva.allInstances->excluding(reserva)->select(estado = 'activa')->collect( r | Tuple{entrada = r.data_de_entrada, saída = r.data_de_saída, n_pessoas = r.número_de_pessoas}), Estadia_Quarto.allInstances->collect( eq | Tuple{entrada = eq.data_de_entrada, saída = eq.data_de_saída, quarto = eq.quarto}) ->union(quartos->collect(q | Tuple{entrada = reserva.data_de_entrada, saída = reserva.data_de_saída, quarto =q.quarto}))),

-- obtém as escolhas de quartos válidas para satisfazer a reserva, ainda sem optimizar -- (para já apenas garante que cada escolha de quartos não tem quartos em excesso) escolhasVálidas : Set(Set(Quarto)) = subconjuntosQuartos(quartosLivres)->select(s | escolhaVálida(s)), in escolhasVálidos->select(s1 | not escolhasVálidas->exists(s2 | Hotel.melhorEscolha(s2, s1) )) -- ver definição de melhorEscolha a seguir


Exemplo: Sistema de Gestão de HotéisDefinição de operação auxiliar para comparar escolhas (1)

context Hotel-- Compara duas escolhas de quartos, devolvendo true se a 1ª for nitidamente melhor que a 2ª-- no sentido de poder maximizar a taxa de ocupação do hotel (aceitar mais estadias/reservas) def: melhorEscolha(escolha1 : Set(Quarto), escolha2 : Set(Quarto)) : Boolean = let -- verifica (recursivamente) se pode colocar um conjunto de grupos (cada grupo representado -- por um inteiro que dá a sua dimensão) num conjunto de quartos (cada quarto representado -- por um inteiro que dá a sua capacidade) podeColocar(dimensõesGrupos: Bag(Integer), capacidadesQuartos: Bag(Integer)): Boolean = dimensõesGrupos->notEmpty() implies let d = dimensõesGrupos->any(true) in capacidadesQuartos->exists (c | podeColocar(if c >= d then dimensõesGrupos->excluding(d) else dimensõesGrupos->excluding(d)->including(d-c) endif, capacidadesQuartos->excluding(c))),

-- da reunião dos quartos de escolha1 e escolha2, obtém os que ficam livres ao optar por escolha1 quartosLivres1 : Set(Quarto) = escolha2 – escolha1,

-- da reunião dos quartos de escolha1 e escolha2, obtém os que ficam livres ao optar por escolha2 quartosLivres2 : Set(Quarto) = escolha1 – escolha2

in escolha1->size() <= escolha2->size() -- optimização and escolha1->collect(capacidade)->sum() <= escolha2->collect(capacidade)->sum() -- optimização and podeColocar( quartosLivres2->collect(capacidade), quartosLivres1->collect(capacidade) ) and not podeColocar( quartosLivres1->collect(capacidade), quartosLivres2->collect(capacidade) ) -- (ver justificação a seguir)


Exemplo: Sistema de Gestão de HotéisDefinição de operação auxiliar para comparar escolhas (2) Justificação:

• Dadas duas escolhas de quartos capazes de satisfazer um pedido, suponhamos que as capacidades dos quartos que ficam livres (quartos não escolhidos) no 1º caso é A={a1, a2, ..., an} e no 2º caso é B={b1, b2, ..., bm}

• Para saber qual dos conjuntos de quartos livres é melhor, temos de determinar duas coisas: (1) Qualquer que seja o conjunto de grupos, se cabe em A então também cabe em B? (2) Qualquer que seja o conjunto de grupos, se cabe em B então também cabe em A?

• O pior caso para (1) (no sentido de caber em A mas poder não caber em B), é quando cada quarto em A fica completamente cheio com um grupo diferente dos outros quartos. Basta por isso testar esse caso. Para determinar (2) também basta testar o caso recíproco.

• A primeira escolha é melhor que a 2ª se se verificar (2) mas não (1)

• Obviamente, a comparação não é prejudicada se se retirarem dos dois conjuntos (A e B) os elementos que são comuns


Definição do corpo de operações de consulta em OCL 2.0 Exemplo:

context Quarto::obterQuartosLivres(entrada: Date, saída : Date, numPessoas : Integer): Set(Quarto)

pre: saída.isAfter(entrada) and numPessoas > 0

body: Quarto.allInstances->select( q | q.capacidade>numPessoas and q.estadia_Quarto->exists(e | DateInterval.disjoint(e.data_de_entrada, e.data_de_saída, entrada, saída, true) )

body: expressão equivale a post: result = expressão

Pós-condição também se poderia indicar mas seria redundante


Pré e pós-condições e herança

O contracto estabelecido pela pré-condição e pós-condição de uma operação não pode ser quebrado pelas sub-classes, isto é:

• a pré-condição pode ser enfraquecida (retirando condições), mas nunca reforçada, numa sub-classe

- uma chamada que era válida do ponto de vista da super-classe tem de continuar a ser válida do ponto de vista da sub-classe

• a pós-condição pode ser reforçada (acrescentando condições), mas nunca enfraquecida, numa sub-classe

- um resultado esperado do ponto de vista da super-classe tem de continuar a ser garantido pela sub-classe

São princípios de "contract-based programming / design / specification" ou "behavioral subtyping"


Definição de valores iniciais em OCL Semelhante a "derive", com "init" em vez de "derive"

Exemplos:• context Reserva::data_da_reserva : Date

init: Date.curDate

• context Reserva::estado : Stringinit: 'activa'

Também se pode indicar directamente o valor inicial no diagrama de classes com

• atributo = valorInicial

versão 4.0


Pós-condições relativas a mensagens enviadas (1) Na pós-condição de uma operação, objecto^mensagem(argumentos)

dá true se a mensagem especificada foi enviada para o objecto especificado durante a execução da operação

Útil para descrever efeito de operação como combinação de alteração de estado interno de um objecto ou sistema, com envio de mensagens para outros objectos ou sistemas externos (cujo estado interno pode ser desconhecido)

• Exemplos: mensagens enviadas para o utilizador (visto como algo externo) e mensagens de callback

• Como restringir as mensagens que podem ser recebidas/processadas dos objectos ou sistemas externos durante a execução da operação?

• No caso de várias mensagens, como restringir a ordem por que as mensagens são enviadas?

• O que acontece se o envio de uma mensagem originar mensagens em sentido inverso, antes de terminar a execução da operação que enviou a primeira mensagem?

A mensagem pode ser do tipo chamada de operação ou envio de sinal (sinais são modelados como classes com estereótipo «signal»)

Se o valor de um argumento não for conhecido ou não for restringido de alguma forma, pode ficar por especificar, usando o símbolo "?" seguido, opcionalmente, do tipo do argumento (para resolução de overloading), como em

observer^update(? : Integer, ? : Integer)

versão 4.0


Pós-condições relativas a mensagens enviadas (2) Na pós-condição de uma operação,

objecto^^mensagem(argumentos) dá a sequência de mensagens do tipo especificado enviadas para o objecto especificado durante a execução da operação

Cada mensagem é do tipo OclMessage Dada uma mensagem m (instância de OclMessage) pode-se aceder ao

valor de um parâmetro p da mensagem com m.p Exemplo no padrão Observer (em que cada instância de Subject tem

registado um conjunto de observers que deve ser notificado com update quando há uma alteração no estado do Subject), supondo que a operação "update" tem parâmetros "i" e "j": context Subject::hasChanged() post: let messages : Sequence(OclMessage) = observers->collect(o | o^^update(? : Integer, ? : Integer) ) in messages->forAll(m | m.i <= m.j )

Operações úteis definidas em OclMessage:• hasReturned() - indica se já retornou de mensagem do tipo chamada de operação

- útil quando a chamada é assíncrona• result() – dá o valor retornado por mensagem do tipo chamada de operação• isSignalSent() – indica se a mensagem é do tipo envio de sinal• isOperationCall() – indica se a mensagem é do tipo chamada de operação

versão 4.0


Verificação formal Provar que os invariantes são compatíveis, isto é, que

a conjunção dos invariantes não dá uma condição impossível

Provar que as pós-condições não violam os invariantes, supondo que o estado inicial obedece aos invariantes e que as pré-condições se verificam

A vantagem de usar uma linguagem como OCL é que possibilita que pelo menos algumas das provas sejam efectuadas automaticamente


Mais informação http://www.fe.up.pt/~jpf/teach/ES - página da disciplina de

Engenharia de Software, com slides sobre UML (organizados por diagramas) e exemplos de análise e desenho orientado por objectos em UML

www.uml.org – especificações e recursos sobre UML, OCL, etc. www.projtech.com – sobre UML executável www.ifad.dk – informação sobre VDM++ e VDMTools The Unified Modeling Language User Guide, Grady Booch et al,

Addison-Wesley, 1998 Business Modeling with UML: Business Patterns at Work, Hans-Erik

Eirksson, Magnus Penker , Wiley, 1999 - boa introdução a OCL Executable UML: A Foundation for Model-Driven Architecture,

Stephne J. Mellor, Marc J. Balcer, Addison-Wesley, 2002 Modelling Systems: Practical Tools and Tecnhiques in Software

Development, John Fitzgerald, Peter Gorm Larsen, Cambridge University Press, 1998 – sobre VDM-SL

Documents

Modelação de Software em Engª de Requisitos, João Pascoal Faria, ERSS, 2003 1 Modelação & Especificação de Sistemas de Software no contexto da Engenharia