Download Lab 1. El contrato de una cola
Document related concepts
no text concepts found
Transcript
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