¿Qué opinas sobre el "lenguaje de programación inteligente" Sketch?
Esto pertenece a la síntesis de programas, que es una rama de aplicación parcial de la verificación formal.
Su lema es permitir que la máquina genere automáticamente programas que cumplan con los requisitos de necesidades (funcionalidad). requisitos de seguridad), y el código generado ha sido verificado formalmente. En teoría, el código que ha sido verificado formalmente no necesita escribir pruebas. Los programadores ya no tienen que devanarse los sesos para pensar en casos de prueba, porque la máquina nos ayuda a verificar el comportamiento. del programa es el esperado bajo todas las entradas posibles. Esta garantía es extremadamente sólida. Si hay una variable en el programa de control de un automóvil autónomo llamada distancia_to_wall (distancia del automóvil a la pared), entonces nuestro código generado lo garantiza. La variable es siempre mayor que 0, por lo que tenemos un coche sin conductor que no chocará contra la pared. Pero la tecnología actual aún no está tan madura, pero los científicos están trabajando duro para lograr este resultado. Todos somos gerentes de productos, por lo que solo tenemos que hacer demandas para los científicos informáticos que han estado buscando la automatización definitiva. Este futuro es muy atractivo, pero como usted dijo, la aplicación sigue siendo relativamente. limitado.
La generación de programas se basa principalmente en la tecnología de resolución de restricciones. Todos han estado expuestos a la resolución de restricciones en la escuela secundaria. Resolver un sistema de ecuaciones lineales es un ejemplo de resolución de restricciones. Resolución: Podemos encontrar que la resolución de restricciones no es un algoritmo, sino un nombre muy general. Para diferentes restricciones, en realidad existen diferentes algoritmos de resolución (procedimiento de decisión). La tecnología de Teorías del módulo de satisfacción integra diferentes algoritmos de resolución. Gao y el Dr. Soonho Kong de la Universidad Carnegie Mellon desarrollaron un solucionador SMT llamado dReal (dReal), que admite ecuaciones diferenciales en restricciones. Casualmente, Sicun Gao es ahora el autor de la investigación Sketch Do en el laboratorio donde trabajo.
La tecnología de generación de programas probablemente consiste en convertir el código fuente en una expresión de restricción, "?" se convierte en una variable desconocida y luego se arroja al solucionador de restricciones para encontrar un conjunto de soluciones, profesor Ras Bodik de la Universidad. de California, Berkeley, ha impartido un curso sobre generación procedimental (Ras Bodik - EECS), puedes consultarlo.