ATS ( Applied Type System ) es un lenguaje de programación diseñado para unificar la programación con una especificación formal. ATS tiene soporte para combinar la demostración de teoremas con la programación práctica mediante el uso de sistemas de tipos avanzados . [2] Una versión anterior de The Computer Language Benchmarks Game ha demostrado que el rendimiento de ATS es comparable al de los lenguajes de programación C y C ++ . [3] Al utilizar la demostración de teoremas y la verificación de tipos estricta, el compilador puede detectar y probar que sus funciones implementadas no son susceptibles a errores como división por cero , pérdidas de memoria ,desbordamiento de búfer y otras formas de corrupción de memoria al verificar la aritmética del puntero y el recuento de referencias antes de que el programa se compile. Además, al utilizar el sistema integrado de demostración de teoremas de ATS (ATS / LF), el programador puede hacer uso de construcciones estáticas que se entrelazan con el código operativo para demostrar que una función alcanza su especificación.
Paradigma | multi-paradigma : funcional , imperativo |
---|---|
Diseñada por | Hongwei Xi en la Universidad de Boston |
Lanzamiento estable | ATS2-0.4.2 [1] / 14 de noviembre de 2020 |
Disciplina de mecanografía | estático |
Licencia | GPLv3 |
Extensiones de nombre de archivo | .sats, .dats, sombreros. |
Sitio web | http://www.ats-lang.org/ |
Influenciado por | |
ML , ML , OCaml , C ++ dependientes |
Historia
ATS se deriva principalmente de los lenguajes de programación ML y OCaml . El lenguaje ha incorporado un lenguaje anterior, ML dependiente , del mismo autor.
La última versión de ATS1 (Anairiats) fue lanzada como v0.2.12 el 2015-01-20. [4] La primera versión de ATS2 (Postiats) se publicó en septiembre de 2013. [5]
Demostración del teorema
El enfoque principal de ATS es respaldar la demostración de teoremas en combinación con la programación práctica. [2] Con la prueba del teorema se puede probar, por ejemplo, que una función implementada no produce pérdidas de memoria. También evita otros errores que, de lo contrario, solo se encontrarían durante las pruebas. Incorpora un sistema similar a los de los asistentes de prueba, que generalmente solo tienen como objetivo verificar las pruebas matemáticas, excepto que ATS usa esta capacidad para probar que las implementaciones de sus funciones operan correctamente y producen el resultado esperado.
Como ejemplo simple, en una función que usa división, el programador puede probar que el divisor nunca será igual a cero, evitando un error de división por cero . Digamos que el divisor 'X' se calculó como 5 veces la longitud de la lista 'A'. Se puede probar que, en el caso de una lista no vacía, 'X' no es cero, ya que 'X' es el producto de dos números distintos de cero (5 y la longitud de 'A'). Un ejemplo más práctico sería demostrar mediante el recuento de referencias que el recuento de retención en un bloque de memoria asignado se cuenta correctamente para cada puntero. Entonces uno puede saber, y probar literalmente, que el objeto no se desasignará prematuramente y que no se producirán pérdidas de memoria .
El beneficio del sistema ATS es que dado que todas las demostraciones de teoremas ocurren estrictamente dentro del compilador, no tiene ningún efecto sobre la velocidad del programa ejecutable. El código ATS es a menudo más difícil de compilar que el código C estándar , pero una vez que se compila, el programador puede estar seguro de que se está ejecutando correctamente en el grado especificado por sus pruebas (asumiendo que el compilador y el sistema de tiempo de ejecución son correctos).
En ATS las pruebas son independientes de la implementación, por lo que es posible implementar una función sin probarla si el programador así lo desea.
Representación de datos
Según el autor (Hongwei Xi), la eficiencia de ATS [6] se debe en gran parte a la forma en que los datos se representan en el lenguaje y las optimizaciones de llamadas finales (que son generalmente importantes para la eficiencia de los lenguajes de programación funcionales). Los datos se pueden almacenar en una representación plana o sin caja en lugar de una representación en caja.
Demostración de teoremas: un caso introductorio
Proposiciones
dataprop
expresa predicados como tipos algebraicos .
Predicados en pseudocódigo algo similar a la fuente ATS (consulte a continuación la fuente ATS válida):
FACT (n, r) iff hecho (n) = r MUL (n, m, prod) sif n * m = prod HECHO (n, r) = HECHO (0, 1) | FACT (n, r) iff FACT (n-1, r1) y MUL (n, r1, r) // para n> 0 // expresa fact (n) = r iff r = n * r1 and r1 = fact (n-1)
En código ATS:
dataprop FACT ( int , int ) = | FACTbas ( 0 , 1 ) // caso básico : FACT ( 0 , 1 ) | { n : int | n > 0 } { r , r1 : int } // caso inductivo FACTind ( n , r ) de ( FACT ( n - 1 , r1 ), MUL ( n , r1 , r ))
donde FACT (int, int) es un tipo de prueba
Ejemplo
No factorial recursiva de cola con proposición o " Teorema " demostrando a través de la construcción dataprop .
La evaluación de fact1 (n-1) devuelve un par (proof_n_minus_1 | result_of_n_minus_1) que se utiliza en el cálculo de fact1 (n). Las pruebas expresan los predicados de la proposición.
Parte 1 (algoritmo y proposiciones)
[FACT (n, r)] implica [fact (n) = r] [MUL (n, m, prod)] implica [n * m = prod]
HECHO (0, 1) FACT (n, r) iff FACT (n-1, r1) y MUL (n, r1, r) para todos n> 0
Recordar:
{...} cuantificación universal[...] cuantificación existencial(... | ...) (prueba | valor)@ (...) tupla plana o tupla de parámetros de función variadic. <...>. métrica de terminación [7]
# incluye "share / atspre_staload.hats"dataprop FACT ( int , int ) = | FACTbas ( 0 , 1 ) of () // caso básico | { n : nat } { r : int } // caso inductivo FACTind ( n + 1 , ( n + 1 ) * r ) de ( FACT ( n , r )) (* tenga en cuenta que int (x), también int x, es el tipo monovaluado del valor int x.La firma de la función a continuación dice: forall n: nat, existe r: int donde fact (num: int (n)) devuelve (FACT (n, r) | int (r)) *)diversión hecho { n : nat } . < n >. ( n : int ( n )) : [ r : int ] ( FACT ( n , r ) | int ( r )) = ( ifcase | n > 0 => (( FACTind ( pf1 ) | n * r1 )) donde { val ( pf1 | r1 ) = hecho ( n - 1 ) } | _ (* más *) => ( FACTbas () | 1 ) )
Parte 2 (rutinas y prueba)
implementar main0 ( argc , argv ) = { val () = if ( argc ! = 2 ) then prerrln ! ( "Uso:" , argv [ 0 ], "" ) val () = afirmar ( argc > = 2 ) val n0 = g0string2int ( argv [ 1 ]) val n0 = g1ofg0 ( n0 ) val () = afirmar ( n0 > = 0 ) val (_ (* pf *) | res ) = hecho ( n0 ) val ( (* void *) ) = println ! ( "hecho (" , n0 , ") =" , res ) }
Todo esto puede agregarse a un solo archivo y compilarse de la siguiente manera. La compilación debería funcionar con varios compiladores de C de back-end, por ejemplo, gcc . La recolección de basura no se usa a menos que se indique explícitamente con -D_ATS_GCATS) [8]
$ patscc fact1.dats -o fact1 $ ./fact1 4
compila y da el resultado esperado
Características
Tipos basicos
- bool (verdadero, falso)
- int (literales: 255, 0377, 0xFF), unario menos como ~ (como en ML )
- doble
- char 'a'
- cadena "abc"
Tuplas y registros
- prefijo @ o ninguno significa asignación directa, plana o sin caja
val x : @ ( int , char ) = @ ( 15 , 'c' ) // x . 0 = 15 ; x . 1 = 'c' val @ ( a , b ) = x // enlace de coincidencia de patrones , a = 15 , b = 'c' val x = @ { first = 15 , second = 'c' } // x . primero = 15 val @ { primero = a , segundo = b } = x // a = 15 , b = 'c' val @ { segundo = b , ...} = x // con omisión , b = 'c'
- prefijo 'significa asignación indirecta o en caja
val x : ' ( int , char ) = ' ( 15 , 'c' ) // x . 0 = 15 ; x . 1 = 'c' val ' ( a , b ) = x // a = 15 , b = ' c ' val x = ' { primero = 15 , segundo = 'c' } // x . primero = 15 val ' { primero = a , segundo = b } = x // a = 15 , b = ' c ' val ' { segundo = b , ...} = x // b = 'c'
- especial
Con '|' como separador, algunas funciones devuelven envuelto el valor del resultado con una evaluación de predicados
val (pruebas_prédicas | valores) = myfunct params
Común
{...} cuantificación universal[...] cuantificación existencial(...) expresión entre paréntesis o tupla(... | ...) (pruebas | valores)
. <...>. métrica de terminación@ (...) tupla plana o tupla de parámetros de función variadic (ver printf del ejemplo )@ [byte] [BUFLEN] tipo de una matriz de valores BUFLEN de tipo byte [9]@ [byte] [BUFLEN] () instancia de matriz@ [byte] [BUFLEN] (0) matriz inicializada a 0
Diccionario
- clasificar
- dominio
sortdef nat = { a : int | a > = 0 } // del preludio : ∀ ' ' a ' ' ∈ int ... typedef String = [ a : nat ] string ( a ) // [..]: ∃ ' ' a ' ' ∈ nat ...
- tipo (como tipo)
- ordenación genérica para elementos con la longitud de una palabra de puntero, que se utilizará en funciones polimórficas con parámetros de tipo. También "tipos en caja" [10]
// {..}: ∀ a, b ∈ tipo ...fun {a, b: type} swap_type_type (xy: @ (a, b)): @ (b, a) = (xy.1, xy.0)
- tipo
- versión lineal del tipo anterior con longitud abstraída. También tipos sin caja. [10]
- tipo de vista
- una clase de dominio como el tipo con una vista (asociación de memoria)
- viewt @ ype
- versión lineal de viewtype con longitud abstraída. Se supersets ViewType
- vista
- relación de un tipo y una ubicación de memoria. El infijo @ es su constructor más común
- T @ L afirma que hay una vista de tipo T en la ubicación L
divertido { a : t @ ype } ptr_get0 { l : addr } ( pf : a @ l | p : ptr l ): @ ( a @ l | a ) fun { a : t @ ype } ptr_set0 { l : addr } ( pf : a ? @ l | p : ptr l , x : a ): @ ( a @ l | void )
- el tipo de ptr_get0 (T) es ∀ l: addr. (T @ l | ptr (l)) -> (T @ l | T) // ver el manual, sección 7.1. Acceso seguro a la memoria mediante punteros [11]
viewdef array_v (a: viewt @ ype, n: int, l: addr) = @ [a] [n] @ l
- T?
- posiblemente tipo no inicializado
exhaustividad de coincidencia de patrones
como en case + , val + , type + , viewtype + , ...
- con el sufijo '+' el compilador emite un error en caso de alternativas no exhaustivas
- sin sufijo, el compilador emite una advertencia
- con '-' como sufijo, evita el control de exhaustividad
modulos
staload "foo.sats" // foo.sats se carga y luego se abre en el espacio de nombres actual staload F = "foo.sats" // para usar identificadores calificados como $ F.bar dynload "foo.dats" // cargado dinámicamente en tiempo de ejecución
vista de datos
Las vistas de datos a menudo se declaran para codificar relaciones definidas de forma recursiva en recursos lineales. [12]
vista de datos array_v (a: viewt @ ype +, int, addr) = | {l: addr} array_v_none (a, 0, l) | {n: nat} {l: addr} matriz_v_algunos (a, n + 1, l) de (a @ l, matriz_v (a, n, l + tamaño de a))
tipo de datos / tipo de vista de datos
Tipos de datos [13]
tipo de datos día de trabajo = Lun | Mar | Mié | Jue | Vie
liza
tipo de datos list0 (a: t @ ype) = list0_cons (a) of (a, list0 a) | list0_nil (a)
tipo de vista de datos
Un tipo de vista de datos es similar a un tipo de datos, pero es lineal. Con un tipo de vista de datos, el programador puede liberar explícitamente (o desasignar) de manera segura la memoria utilizada para almacenar los constructores asociados con el tipo de vista de datos. [14]
variables
variables locales
var res: int con pf_res = 1 // introduce pf_res como un alias de view @ (res)
en la asignación de matriz de pila :
#define BUFLEN 10var! p_buf con pf_buf = @ [byte] [BUFLEN] (0) // pf_buf = @ [byte] [BUFLEN] (0) @ p_buf [15]
Ver declaraciones val y var [16]
Referencias
- ^ Hongwei Xi (14 de noviembre de 2020). "[ats-lang-users] ATS2-0.4.2 lanzado" . ats-lang-users . Consultado el 17 de noviembre de 2020 .
- ^ a b Combinando programación con demostración de teoremas
- ^ Puntos de referencia de ATS | Juego de comparativas de lenguaje informático (archivo web)
- ^ "El sistema ATS PL - Examinar / Ats-lang en SourceForge.net" .
- ^ "Actualización: agregar un archivo de versión. · Githwxi / ATS-Postiats @ 30fd556" .
- ^ Discusión sobre la eficiencia del lenguaje (Language Shootout: ATS es el nuevo pistolero superior. Beats C ++.)
- ^ Métricas de terminación
- ^ Compilación: recolección de basura Archivado el 4 de agosto de 2009 en la Wayback Machine.
- ^ tipo de una matriz Archivado el 4 de septiembre de 2011 en lostipos de Wayback Machine como @ [T] [I]
- ^ a b "Introducción a los tipos dependientes" . Archivado desde el original el 12 de marzo de 2016 . Consultado el 13 de febrero de 2016 .
- ^ Manual, sección 7.1. Acceso seguro a la memoria a través de punteros [ enlace muerto permanente ] (desactualizado)
- ^ Construcción de Dataview Archivado el 13 de abril de 2010 en la Wayback Machine.
- ^ Construcción de tipo de datos Archivado el 14 de abril de 2010 en la Wayback Machine.
- ^ Construcción de tipo de vista de datos
- ^ Manual - 7.3 Asignación de memoria en la pila Archivado el 9 de agosto de 2014 en Wayback Machine (desactualizado)
- ^ Declaraciones de Val y Var Archivadas el 9 de agosto de 2014 en Wayback Machine (desactualizado)
enlaces externos
- Página de inicio de ATS
- La documentación del lenguaje de programación ATS para ATS2
- La documentación antigua del lenguaje de programación ATS para ATS1
- Borrador manual (desactualizado). Algunos ejemplos se refieren a funciones o rutinas que no están presentes en la versión (Anairiats-0.1.6) (por ejemplo: sobrecarga de impresión para strbuf, y el uso de sus ejemplos de matriz da errmsgs como "no se admite el uso de la suscripción de matriz").
- ATS para programadores de ML
- Ejemplos de aprendizaje y casos de uso breves de ATS