Spec Sharp - Spec Sharp
| Paradigma | multi-paradigma : estructurado , imperativo , orientado a objetos , impulsado por eventos , funcional , contrato |
|---|---|
| Diseñada por | Investigación de Microsoft |
| Desarrollador | Investigación de Microsoft |
| Apareció por primera vez | 2004 |
| Lanzamiento estable | SpecSharp 2011-10-03 / 7 de octubre de 2011
|
| Disciplina de mecanografía | estático , fuerte , seguro , nominativo |
| Licencia | Acuerdo de licencia de fuente compartida de Microsoft Research (MSR-SSLA) |
| Sitio web | investigación |
| Influenciado por | |
| C # , Eiffel | |
| Influenciado | |
| Canta# | |
Spec # es un lenguaje de programación con características de lenguaje de especificación que amplía las capacidades del lenguaje de programación C # con contratos tipo Eiffel , incluidos objetos invariantes , precondiciones y poscondiciones. Al igual que ESC / Java , incluye una herramienta de verificación estática basada en un demostrador de teoremas que puede verificar estáticamente muchos de estos invariantes. También incluye una variedad de otras extensiones menores del lenguaje, como tipos de referencia no nulos.
La API de contratos de código en .NET Framework 4.0 ha evolucionado con Spec #.
Microsoft Research desarrolló tanto Spec # como C # ; a su vez, Spec # sirve como base del lenguaje de programación Sing # , que Microsoft Research también desarrolló.
Características
Spec # extiende el lenguaje de programación central C # con características como:
- Tipos que no aceptan valores NULL
- Estructuras para contratos de código como condiciones previas y condiciones posteriores .
- Se verificaron excepciones similares a las de Java .
- Sintaxis conveniente
Ejemplo
Este ejemplo muestra dos de las estructuras básicas que se utilizan al agregar contratos a su código ( pruebe Spec # en su navegador ).
static int Main(string![] args)
requires args.Length > 0;
ensures return == 0;
{
foreach(string arg in args)
{
Console.WriteLine(arg);
}
return 0;
}
- ! se utiliza para hacer un tipo de referencia no anulable, por ejemplo, no puede establecer el valor en nulo. Esto a diferencia de los tipos que aceptan valores NULL, que permiten que los tipos de valor se establezcan como nulos .
- require indica una condición previa que debe seguirse en el código. En este caso, no se permite que la longitud de los argumentos sea cero o menor.
- asegura indica una condición posterior que debe seguirse en el código.
Canta#
Sing # es un superconjunto de Spec #. Microsoft Research desarrolló Spec #, y luego lo extendió a Sing # para desarrollar el sistema operativo Singularity . Sing # aumenta las capacidades de Spec # con soporte para canales y construcciones de lenguaje de programación de bajo nivel , que son necesarios para implementar el software del sistema . Sing # es seguro para escribir. La semántica de las primitivas de paso de mensajes en Sing # se define mediante contratos formales y escritos.
Fuentes
- Barnett, M., KRM Leino, W. Schulte, "El sistema de programación Spec #: una descripción general". Actas de Construcción y Análisis de Dispositivos Inteligentes Seguros, Protegidos e Interoperables (CASSIS) , Marsella. Springer-Verlag , 2004.