Spec

No enciclopédico 1 Introducción Spec es un sistema de programación con el objetivo de extender el potencial de C (como en el caso de Eiffel con los contratos), incluyendo invariantes de objetos, precondiciones y poscondiciones. Como ESC/Java este incluye una herramienta de chequeo estático que es capaz de verificar estáticamente muchas de esas invariaciones. Este también incluye una variedad de extensiones menores para el lenguaje, como los tipos de referencia no nula. Este es un proyecto creado con la intención de estudiar la posibilidad de incluir la metodología del Diseño por Contrato primeramente en C, para después, en dependencia de los resultados, incluirlo en todos los lenguajes de .NET. Microsoft actualmente tiene separado dos grupos de investigación en Microsoft Research estudiando ambas posibilidades, uno lleva por nombre Código por Contrato (Code Contract) y el segundo, como podemos imaginar, se le llamo Spec. En estos momentos los creadores de C no han hecho ningún pronunciamiento acerca de la posibilidad de que aparezca este nuevo rasgo en C 4.0, pero parece ser de que existe una posibilidad real de que pudiera aparecer, aunque estas son puras especulaciones mías. La mayoría de los investigadores que forman parte de este proyecto, como una gran parte de Microsoft Research, son profesores de Universitarios como Mike Barnet. Otro que ha jugado un rol principal en la creación y divulgación de Spec es Rustan M. Leino, el cual trabaja ya desde hace varios años para Microsoft Research en Redmond. El sistema de programación Spec es una nueva tentativa a mejorar el desarrollo y el mantenimiento de software de alta calidad. Este seminario veremos en qué consiste el Sistema de Programación Spec, el cual está conformado por: ? El lenguaje de Programación: Es una extensión de C con tipos no nulos, excepciones verificadas y clausulas throws, métodos por contrato e invariantes de objetos.