Download Lab 1. El contrato de una cola

escuela técnica superior
de ingeniería informática
Implementación
metódica de
contratos semánticos
Departamento de
Lenguajes y Sistemas Informáticos
Ingeniería del Software II
Índice
 Introducción
 Ejemplo Queue
 Interfaz e implementación
 Contrato semántico
 Implementación del contrato
 Guía general
 Condiciones
 Automatización de las pruebas
Índice
 Introducción
 Ejemplo Queue
 Interfaz e implementación
 Contrato semántico
 Implementación del contrato
 Guía general
 Condiciones
 Automatización de las pruebas
Introducción
 Implementación metódica
 Características:
 Implementación en Java
 Contrato semántico como una decoración
 Evaluación de las condiciones con Asserts
 JUnit para la automatización de pruebas
 Trabajo en dos etapas
 Contrato sin modelo (hoy)
 Contrato con modelo (próxima clase)
Índice
 Introducción
 Ejemplo Queue
 Interfaz e implementación
 Contrato semántico
 Implementación del contrato
 Guía general
 Condiciones
 Automatización de las pruebas
Ejemplo Queue
<< interface >>
IQueue
+first():Object
+append(o:Object):void
+delete():void
+size():int
- obj
Queue
#q:LinkedList
<< create >>+Queue():Queue
+first():Object
+append(o:Object):void
+delete():void
+size():int
QueueSem
-nestingLevel:int
-pre$delete$size :int
-pre$append$size :int
-pre$append$first:Object
<< create >>+QueueSem (obj:IQueue ):QueueSem
-queue$init ():void
-pre$first():void
+first():Object
-post$first(first$result:Object):void
-pre$append(o:Object):void
+append(o:Object):void
-post$append(o:Object):void
-pre$delete():void
+delete():void
-post$delete():void
-pre$size():void
+size():int
-post$size(size$output:int):void
-queue$inv ():void
Created with Poseidon for UML Community Edition. Not for Commercial Use.
Índice
 Introducción
 Ejemplo Queue
 Interfaz e implementación
 Contrato semántico
 Implementación del contrato
 Guía general
 Condiciones
 Automatización de las pruebas
Interfaz
<< interface >>
IQueue
+first():Object
+append(o:Object):void
+delete():void
+size():int
- obj
Queue
#q:LinkedList
<< create >>+Queue():Queue
+first():Object
+append(o:Object):void
+delete():void
+size():int
QueueSem
-nestingLevel:int
-pre$delete$size :int
-pre$append$size :int
-pre$append$first:Object
<< create >>+QueueSem (obj:IQueue ):QueueSem
-queue$init ():void
-pre$first():void
+first():Object
-post$first(first$result:Object):void
-pre$append(o:Object):void
+append(o:Object):void
-post$append(o:Object):void
-pre$delete():void
+delete():void
-post$delete():void
-pre$size():void
+size():int
-post$size(size$output:int):void
-queue$inv ():void
Created with Poseidon for UML Community Edition. Not for Commercial Use.
Interfaz
IQueue.java
public interface IQueue {
Object first();
void append(Object o);
void delete();
int size();
}
Posible implementación
Queue.java
public class Queue implements IQueue {
protected LinkedList q; // Ojo al protected
public Queue() {
q = new LinkedList();
}
public Object first() {
return q.getFirst();
}
public void append(Object o) {
q.addLast(o);
}
...
Posible implementación
Queue.java
...
public void delete() {
q.removeFirst();
}
public int size() {
return q.size();
}
}
Índice
 Introducción
 Ejemplo Queue
 Interfaz e implementación
 Contrato semántico
 Implementación del contrato
 Guía general
 Condiciones
 Automatización de las pruebas
Contrato semántico
contract IQueueSem on IQueue {
@query first, size
@inv true // Lo cambiaremos en la siguiente clase
result first() {
@pre size() > 0
@post true
}
append(o) {
@pre true
@post size()@pre == 0 ==> first() == o
@post size()@pre > 0 ==> first() == first()@pre
@post size() == size()@pre + 1
}
...
Contrato semántico
...
delete() {
@pre size() > 0
@post size() == size()@pre – 1
}
result size() {
@pre true
@post result >= 0
}
IQueue() { // Ojo, no visto en teoría
@post size() == 0
}
}
Implementación
<< interface >>
IQueue
+first():Object
+append(o:Object):void
+delete():void
+size():int
- obj
Queue
#q:LinkedList
<< create >>+Queue():Queue
+first():Object
+append(o:Object):void
+delete():void
+size():int
QueueSem
-nestingLevel:int
-pre$delete$size :int
-pre$append$size :int
-pre$append$first:Object
<< create >>+QueueSem (obj:IQueue ):QueueSem
-queue$init ():void
-pre$first():void
+first():Object
-post$first(first$result:Object):void
-pre$append(o:Object):void
+append(o:Object):void
-post$append(o:Object):void
-pre$delete():void
+delete():void
-post$delete():void
-pre$size():void
+size():int
-post$size(size$output:int):void
-queue$inv ():void
Created with Poseidon for UML Community Edition. Not for Commercial Use.
Índice
 Introducción
 Ejemplo Queue
 Interfaz e implementación
 Contrato semántico
 Implementación del contrato
 Guía general
 Condiciones
 Automatización de las pruebas
Guía general
<< interface >>
IQueue
+first():Object
+append(o:Object):void
+delete():void
+size():int
- obj
Queue
#q:LinkedList
<< create >>+Queue():Queue
+first():Object
+append(o:Object):void
+delete():void
+size():int
QueueSem
-nestingLevel:int
-pre$delete$size :int
-pre$append$size :int
-pre$append$first:Object
<< create >>+QueueSem (obj:IQueue ):QueueSem
-queue$init ():void
-pre$first():void
+first():Object
-post$first(first$result:Object):void
-pre$append(o:Object):void
+append(o:Object):void
-post$append(o:Object):void
-pre$delete():void
+delete():void
-post$delete():void
-pre$size():void
+size():int
-post$size(size$output:int):void
-queue$inv ():void
Created with Poseidon for UML Community Edition. Not for Commercial Use.
Llamada al método decorado
QueueSem.java
...
public void append(Object o) {
if (nestingLevel == 0)
pre$append(o);
pre$append$size = obj.size();
if (pre$append$size > 0)
pre$append$first = obj.first();
nestingLevel++;
obj.append(o);
nestingLevel--;
if (nestingLevel == 0) {
post$append(o);
queue$inv();
}
}
...
llamada a la Pre/Post e invariante
QueueSem.java
...
public void append(Object o) {
if (nestingLevel == 0)
pre$append(o);
pre$append$size = obj.size();
if (pre$append$size > 0)
pre$append$first = obj.first();
nestingLevel++;
obj.append(o);
nestingLevel--;
if (nestingLevel == 0) {
post$append(o);
queue$inv();
}
}
...
Semántica transaccional
QueueSem.java
...
public void append(Object o) {
if (nestingLevel == 0)
pre$append(o);
pre$append$size = obj.size();
if (pre$append$size > 0)
pre$append$first = obj.first();
nestingLevel++;
obj.append(o);
nestingLevel--;
if (nestingLevel == 0) {
post$append(o);
queue$inv();
}
}
...
Evaluación del preestado
QueueSem.java
...
public void append(Object o) {
if (nestingLevel == 0)
pre$append(o);
pre$append$size = obj.size();
if (pre$append$size > 0)
pre$append$first = obj.first();
nestingLevel++;
obj.append(o);
nestingLevel--;
if (nestingLevel == 0) {
post$append(o);
queue$inv();
}
}
...
Índice
 Introducción
 Ejemplo Queue
 Interfaz e implementación
 Contrato semántico
 Implementación del contrato
 Guía general
 Condiciones
 Automatización de las pruebas
Condiciones
 Usaremos AssertTrue definido en JUnit
(junit.framework.Assert) para evaluar
condiciones
public static void
assertTrue(String message, boolean condition)
 Evalua condition, si es falsa, lanza la
excepción AssertionFailedError con el
mensaje message
 Las condiciones se expresan en Java
Precondiciones
QueueSem.java
...
private void pre$append(Object o) {
Assert.assertTrue("@pre true", true);
}
...
Postcondiciones
QueueSem.java
...
private void post$append(Object o) {
Assert.assertTrue(
"@post size() == size()@pre + 1",
obj.size() == pre$append$size + 1);
Assert.assertTrue(
"@post size()@pre == 0 ==> first() == o”,
!(pre$append$size == 0) || obj.first() == o);
Assert.assertTrue(
"@post size()@pre > 0 ==> first() == first()@pre”,
!(pre$append$size > 0) ||
obj.first() == pre$append$first);
}
...
Invariantes
QueueSem.java
...
private void queue$inv(Object o) {
Assert.assertTrue("@inv true", true);
}
...
Condiciones iniciales
QueueSem.java
...
private void queue$init(Object o) {
Assert.assertTrue("@post size()==0", obj.size()==0);
}
...
public QueueSem(IQueueModel obj) {
this.obj = obj;
nestingLevel = 0;
queue$init();
}
...
Índice
 Introducción
 Ejemplo Queue
 Interfaz
 Modelo
 Contrato semántico
 Implementación del contrato
 Guía general
 Condiciones
 Automatización de las pruebas
Automatización de las pruebas
 Incluir la biblioteca:
 eclipse\plugins\org.junit_3.8.1
 Definir una clase de prueba que extienda
junit.framework.TestCase, donde se
defina un posible escenario de uso de la
interfaz
 Ejecutar la prueba: Run/Run As/Junit
Test
Pruebas
TestsQueue.java
public class TestsQueue extends TestCase {
public void testFirst1() {
IQueue q = new QueueSem(new Queue());
String e0 = "Cadena 0";
q.append(e0);
}
public void testFirst2() {
IQueue q = new QueueSem(new Queue());
q.first();
}
...
}
!Gracias!
 ¿Podemos mejorar esta lección?
 Escríbenos al foro de la asignatura
 Visita la web de la asignatura