Los contratos para Java le permite anotar el código de los contratos en forma deprecondiciones, postcondiciones e invariantes.
Estas anotaciones del contrato son fácil de leer y escribir, y comprobar en tiempo de ejecución.
Anotar el código de los contratos le ayuda a:
diseño, documento, probar, y depurar sus programas.
He aquí un ejemplo simple de una clase Java, con la anotación de contratos:
interface Time {
...
@Ensures({
"result >= 0",
"result <= 23"
})
int getHour();
@Requires({
"h >= 0",
"h <= 23"
})
@Ensures("getHour() == h")
void setHour(int h);
...
}Esto es lo que el contrato es:
|
Obligación |
Beneficio |
Método de Llamado |
Satisfacer condición; Asegúrese de que la 'h' no es ni muy pequeño ni muy grande |
(De postcondición) GetHour () devuelve h. |
Método de Llamado |
Satisfacer postcondición; Debe hacer GetHour h () devuelven .. |
(De la condición) puede asumir h no es ni muy pequeño ni muy grande. |
Para utilizar Cofoja que hay que hacer las dos cosas siguientes:
Download one of the JARs (O tomar un unofficial build; ver FAQ para mayor información)
Ver el archivo readme, a continuación:
Los contratos de Java es un marco de programación para Java contrato, que utiliza técnicas de procesamiento de anotación y la instrumentación de bytecode para proporcionar tiempo de ejecución de la comprobación.
Contratos fo Java requiere Java versión 6 para el procesamiento de anotación y el código de bytes de la instrumentación. La re-escritura de código de bytes depende de la ASM biblioteca de manipulación de código de bytes, la versión 3.2 o superior.
Puesto que el agente de Java bytecode reescribe con el fin de inyectar los contratos en el código cargado, la biblioteca ASM tiene que estar disponible en el la ruta de clase en tiempo de ejecución del contrato si la comprobación se hace cumplir a través de la agente. Pre-contratados archivos de clase no es necesario la biblioteca o el ASM agente se ejecute con los contratos habilitados.
Para que el script de generación para funcionar correctamente, usted debe por lo menos especificar la ruta correcta a las dependencias Cofoja en el local de construcción
Este archivo no existe de forma predeterminada, puede o bien crear o iniciar a partir de una copia del archivo de configuración por defecto:
Este archivo también contiene todas las propiedades configurables por el usuario con su descripciones y los valores predeterminados. Una vez que hayas terminado, establece lo siguiente propiedad en true para permitir que la hormiga ejecutar:
Para crear un archivo JAR que contiene todas las clases Cofoja, ejecute:
El archivo JAR se encuentra en:
./dist/lib/cofoja- <versión>. jar
Puede ser utilizado tanto como un agente de Java y procesador anotación y debe añadirse a la ruta de clase.
Para compilar el código con las anotaciones del contrato, ejecute:
javac -processor com.google.java.contract.core.apt.AnnotationProcessor <someclass>.java
Para ejecutar el código compilado con contrato de comprobación habilitada, asegúrese de que el archivos generados (adicional. clase y los archivos. contratos) son en su ruta de la clase, y ejecutar:
java -javaagent:path/to/cofoja-<version>.jar <someclass>
Los contratos de Java es anotado con sus propios contratos, que puede ser compilado, probado y empaquetado en el archivo JAR resultado por lo que comprueba su propios contratos se usan para elaborar los contratos y el control de su programa!
Tenga en cuenta que la ejecución de una construcción será necesariamente más lento que ejecutando una versión sin control de los Contratos de Java, pero es una gran manera para que usted pueda contribuir con el proyecto, ayudando a ejercer su propia capacidades durante su uso.
Para construir una versión contraída de los Contratos de Java, es necesario tener Cofoja un archivo JAR listos en primer lugar (véase la sección anterior, o podría reutilizar una que se ha construido con una ejecución anterior de este arranque proceso). Copie el archivo JAR:
Una vez que la versión completa es contratado, puede ejecutar el conjunto de pruebas con:
Además de la auto-contratado construcciones, archivos JAR Cofoja incluido con ASM clases de biblioteca también se puede producir, en aras de la más fácil distribución:
ant -Dasmjar=path/to/asm-all-<version>.jar dist
Los contratos para Java se compone de un procesador de anotación, una agente de instrumentación, así como una regrabadora bytecode desconectado. La procesador de anotación recoge anotaciones en la clase de contrato separado archivos. El agente de instrumentación teje estos expedientes de los contratos con la clases reales antes de que se cargan en la JVM. Alternativamente, el re-escritura de código de bytes en línea puede ser utilizada para producir la clase de pre-tejida archivos que pueden ser desplegados directamente sin ningún tipo de dependencia Cofoja.
Las siguientes instrucciones asumen que usted tiene el JAR Cofoja y ASM archivos en su ruta de clase.
El procesador de punto anotación de entrada es (para uso con el procesador)
com.google.java.contract.core.apt.AnnotationProcessor
El agente de Java puede ser invocado desde el fichero JAR compilado (para su uso con el-javaagent java opción):
./dist/cofoja-<version>.jar
El instrumentador en línea se puede ejecutar con:
java -Dcom.google.java.contract.classoutput=<outdir> \
com.google.java.contract.core.agent.PreMain <someclass>.class
Por favor, consulte la documentación oficial en línea para obtener más información:
http://code.google.com/p/cofoja/wiki/QuickReference
Los contratos de Java es un proyecto muy joven. Por favor, ayúdenos a hacer mejor informar de los fallos y la publicación de parches en:
http://code.google.com/p/cofoja/issues/
Añadir los contratos a sus clases
Traducción:
Una interfaz de pila contratado
Primero vamos a definir una interfaz minimalista pila. Una pila deberán incluir al menos los métodos para insertar un nuevo elemento en la parte superior de la misma, y quitar el elemento de la cima:
interface Stack<T> {
public T pop();
public void push(T obj);
}Si se trata de contraer esta interfaz, sin embargo, nos encontraremos con ningún contrato obvio para poner en él. Esto es debido a que la interfaz expone un método de consulta que nos permite examinar el estado del objeto, sin cambiarla. Con el fin de establecer los contratos sobre el estado de un objeto, es necesario ser capaz de consultar ese estado.
Una simple información que puede querer hacer afirmaciones sobre el número de elementos en la actualidad en una pila. Vamos a añadir un método a nuestro tamaño de la interfaz:
interface Stack<T> {
public int size();
public T pop();
public void push(T obj);
}En Java, int es un tipo entero con signo, pero es bastante obvio que una pila puede nunca tener un número negativo de elementos: vamos a escribir que, como nuestro primer contrato! Dado que es un contrato en el estado de un objeto que siempre se mantiene, debe ser una clase invariante; invariantes de clase se denotan por el com.google.java.contract.Invariant anotación.
import com.google.java.contract.Invariant;
@Invariant("size() >= 0")
interface Stack<T> {
public int size();
public T pop();
public void push(T obj);
}
Nota: Tenga en cuenta las cotizaciones en torno a la expresión de los idiomas. Este es un artefacto sintáctico debido a la forma anotaciones se manejan en Java. Los valores de anotación que ser constantes y sólo puede ser manipulado como tal, por lo tanto, las expresiones deben estar encerrados en una cadena literal. Ellos están obligados a ser válido el código de Java, sin embargo (con unas pocas extensiones, más sobre esto más adelante).
No hay más que podemos expresar con sólo esta información simple, sin embargo. No permitir hacer estallar la pila cuando no hay elementos en que parece como un contrato de sonido. Dado que es un requisito sobre el estado del objeto antes de la invocación de un método, que debería ser una condición previa método; condiciones previas se indican con la anotación com.google.java.contract.Requires.
import com.google.java.contract.Requires;
@Invariant("size() >= 0")
interface Stack<T> {
public int size();
@Requires("size() >= 1")
public T pop();
public void push(T obj);
}
Pero también lo desea, puede hacer valer las cosas en el estado del objeto después de la invocación de un método. En este ejemplo, se sabe que una vez que un elemento ha sido reventado, la pila es un elemento más pequeño, y una vez un elemento ha sido empujado en él, es un elemento más grande. Para escribir esto, necesitamos un método de postcondición, denotado por la anotación
com.google.java.contract.Ensures:
import com.google.java.contract.Ensures;
import com.google.java.contract.Invariant;
import com.google.java.contract.Requires;
@Invariant("size() >= 0")
interface Stack<T> {
public int size();
@Requires("size() >= 1")
@Ensures("size() == old(size()) - 1")
public T pop();
@Ensures("size() == old(size()) + 1")
public void push(T obj);
}
Esta iteración introduce dos nuevos elementos: el Garantiza la anotación y la vieja palabra. El Asegura la anotación, simplemente delimita la condición posterior, como hemos visto antes con Requiere y Invariante . La vieja palabra clave dentro de la expresión postcondición es una de las pocas extensiones a la sintaxis de Java con el apoyo de nuestro marco.
La palabra clave vieja le permite examinar los viejos valores, es decir, los valores de las expresiones como estaban antes de la invocación del método. Una llamada a este método de pseudo-devuelve el valor de su argumento expresión, ya que eran antes de la ejecución del método actual.
Esto es lo más lejos que vamos, sin embargo, con sólo el tamaño de la pila como una información recuperable. Con sólo esta descripción, un simple contador sería capaz de engañar a nuestros contratos. Pero ya que el propósito del diseño por contrato no es la especificación completa de sus programas, que pueden o no quieren dejar aquí, o incluso antes en uno de los pasos. Con el fin de demostrar más características de nuestro marco fresco, sin embargo, vamos a añadir otro método de consulta. :-)
Imagina que quieres más fuertes en su pila de contratos, contratos que no sólo involucran el tamaño de la colección, sino también su contenido.Usted puede introducir un método de consulta que devuelve una copia completa de los contenidos de la pila como una lista, pero recuerde que esto podría o no ser conveniente para las clases que implementan esta interfaz. En este sentido, optar por añadir un método de mirar más ligero, que devuelve el objeto superior sin que explote la misma. Sus requisitos son los mismos que los del pop.
.
import com.google.java.contract.Ensures;
import com.google.java.contract.Invariant;
import com.google.java.contract.Requires;
@Invariant("size() >= 0")
interface Stack<T> {
public int size();
@Requires("size() >= 1")
public T peek();
@Requires("size() >= 1")
@Ensures("size() == old(size()) - 1")
public T pop();
@Ensures("size() == old(size()) + 1")
public void push(T obj);
}
Usando vistazo , podemos establecer que un objeto extrae de la pila debe ser el mismo que el que estaba previamente en la parte superior y, análogamente, que un objeto sólo inserta en la pila es el elemento superior nuevo. Nuestra interfaz se convierte en:
import com.google.java.contract.Ensures;
import com.google.java.contract.Invariant;
import com.google.java.contract.Requires;
@Invariant("size() >= 0")
interface Stack<T> {
public int size();
@Requires("size() >= 1")
public T peek();
@Requires("size() >= 1")
@Ensures({
"size() == old(size()) - 1",
"result == old(peek())"
})
public T pop();
@Ensures({
"size() == old(size()) + 1",
"peek() == old(obj)"
})
public void push(T obj);
}
Este cambio ilustra la forma en varias cláusulas puede ser colocado en una sola condición posterior. La misma sintaxis puede, por supuesto, ser utilizados para los invariantes y las condiciones previas. Las distintas cláusulas se asocian con un AND. También cuenta con el resultado reservada variable, que contiene el valor devuelto por el método contratado, sino que es, por supuesto, sólo se puede acceder en condiciones posteriores y sólo si el método devuelve algo (es decir, no nula).
La interfaz que resulta ahora más o menos utiliza todos los contratos construye a disposición de una sola clase. Pero hay algo más que sólo a los contratos de invariantes, precondiciones y postcondiciones de una sola clase! Vamos a continuar nuestro recorrido por la aplicación de una pila de concreto.
Una implementación de la pila contratado
Echemos un vistazo a una implementación sencilla que consiste en una envoltura alrededor de un objeto ArrayList:
import com.google.java.contract.Ensures;
import com.google.java.contract.Invariant;
import java.util.ArrayList;
@Invariant("elements != null")
public class ArrayListStack<T> implements Stack<T> {
protected ArrayList<T> elements;
public ArrayListStack() {
elements = new ArrayList<T>();
}
public int size() {
return elements.size();
}
public T peek() {
return elements.get(elements.size() - 1);
}
public T pop() {
return elements.remove(elements.size() - 1);
}
@Ensures("elements.contains(old(obj))")
public void push(T obj) {
elements.add(obj);
}
}
Esta clase tiene casi ningún contrato de sí mismo, pero hereda todos los contratos de la pila de interfaz que implementa. Un tipo contratado hereda todos los contratos de todos sus padres (superclases e interfaces implementadas).
La herencia de contrato que le permite compartir y contratos de la mezcla. Se puede ver como una extensión del mecanismo de interfaz (aunque funciona en superclases también) del núcleo del lenguaje Java, añadiendo afirmaciones arbitrarias a su poder especificación.
Además, los contratos pueden ser refinados. Si volvemos a nuestro ejemplo, podemos ver que un invariante y una postcondición se han añadido.A diferencia de método de alteración temporal, estos nuevos contratos no sustituyen a las heredadas a través de la pila . En su lugar, se combinan de acuerdo con la tabla siguiente:
Estas reglas se derivan intuitivamente desde el hecho de que un submétodo anular una supermethod puede aceptar la entrada de los contravariantes y covariantes producir una salida. En otras palabras, un método, siempre se debe aceptar por lo menos ya que muchos estados y los argumentos en la entrada como su padre (de ahí el contrato sólo puede aflojar), y deben garantizar como mínimo tanto como su padre (de ahí el contrato no puede sino reforzar), por lo que que con seguridad se puede utilizar desde un sitio de llamadas que asume el contrato de su supermethod.
Otro punto a destacar es el hecho de que nuestros nuevos contratos se refieren a un campo de protección. Un contrato comparte el mismo alcance que la declaración del método que se aplica a (es decir, haciendo caso omiso de lo que pueda ser declarada en el cuerpo del método), y por lo tanto puede acceder a las mismas variables y llamar a los mismos métodos. Acceso a los miembros del restringido está permitido, pero usted debe hacer sus contratos públicos siempre que sea posible, para que puedan servir como documentación externa. Por otra parte, la práctica de referirse a los miembros restringidos se recomienda en el interior de las condiciones previas, en las que no tiene mucho sentido: si el método depende de un estado interno de precisión para ejecutar, se debe considerar la posibilidad de una forma de consulta que el Estado, como parte de su interfaz.
A continuación más información acerca de Cofoja:
Add support for contracts to your Ant project
Quick reference
Fine tune the runtime checking of contracts
How to write good contracts
Frequently asked questions
Using Contracts with Eclipse (external link, thanks to Fabian Steeg)
Using Contracts with IntelliJ IDEA (external link, java
Gestos Lockscreen
Gafas de teléfono
OpenVPN
Incógnito Modo
Temas de Apoyo
DSP Ecualizador