Herramientas
Git es una herramienta de código abierto para control de versiones, siguiendo un modelo distribuido (al contrario de herramientas como SVN que siguen un modelo cliente-servidor) y descentralizado. Al trabajar con Git se tienen repositorios locales que pueden usar un repositorio remoto para sincronizar los cambios. En general, lo más común es tener algún repositorio remoto, en esta materia vamos a utilizar GitHub como repositorio remoto.
En Linux/Unix deberían poder utilizar el manejador de paquetes por defecto, apt o snap para distros basadas en Debian, pacman para distros basadas en Arch, entre otros. Por ejemplo, en Ubuntu pueden utilizar:
sudo apt install git
En Windows pueden seguir las instrucciones en esta página; pueden instalar Git para Windows; y otra opción es usar SmartGit que es gratis para el ámbito educativo.
Para Mac OS X pueden seguir las instrucciones en esta página.
Dafny es un lenguaje desarrollado por el grupo RiSE de Microsoft. Dafny es un lenguaje multi-paradigma que toma inspiración y características de diversos lenguajes, ofreciendo entre las mismas a: herencia de clases y características; tipos de datos inductivos que pueden tener métodos asociados y son apropiados para pattern matching; tipos de datos inductivos con evaluación perezosa, estos permiten definir valores potencialmente infinitos (por ejemplo: una lista de 1s que no tiene un tamaño definido); tipos restringidos por predicados, dado un tipo A, es posible definir un tipo B como B = {x : A | P(x)} que significa B es el conjunto de todos los valores en A tal que se cumple el predicado P para cada uno de ellos, un ejemplo son los naturales definidos como Nat = {x : Int | x >= 0}; lambdas, que representan funciones anónimas, ej.: \x, y -> x + y como la función anónima que suma dos valores; y finalmente estructuras de datos mutables e inmutables, como conjuntos, listas, etc.
A su vez, y la característica de interés para esta materia, es que Dafny soporta no solamente escribir especificaciones formales junto al código de los programas, sino que además soporta verificación automática de las mismas.
A continuación se muestra un ejemplo de una función que calcula el valor absoluto Abs con su especificación asociada.
Este ejemplo fue sacado del repositorio GitHub de Dafny.
La instalación de Dafny como extensión de Visual Studio Code es simple, requiere ir a la sección de extensiones, buscar dafny, e instalar la extensión.
Las instrucciones se dan en el contexto de Ubuntu, para otras distros se pueden utilizar las páginas provistas para buscar los cambios necesarios.
En esta página web están las instrucciones para instalar .NET en distintas versiones de Ubuntu. Solo es necesaria la instalación de las librerías de Runtime.
- Descargar el instalador
.debdesde la página web de Visual Studio Code. - Instalar Visual Studio Code utilizando el archivo
.debdescargado:- Mediante el instalador de software: click derecho en el archivo
.deb-> "abrir con" -> Software Install. - Por terminal:
- Mediante el instalador de software: click derecho en el archivo
sudo dpkg -i /absolute/path/to/deb/file
sudo apt-get install -f
Siga las instrucciones para la instalación de Dafny para su uso por terminal.
En esta página web están las instrucciones para instalar .NET en distintas versiones de Windows. Solo es necesaria la instalación de las librerías de Runtime.
En Windows pueden descargar el instalador para Visual Studio Code.
Siga las instrucciones para la instalación de Dafny para su uso por terminal.
En esta página web están las instrucciones para instalar .NET en distintas versiones de macOS (10.15+). Solo es necesaria la instalación de las librerías de Runtime.
En macOS pueden descargar el instalador para Visual Studio Code.
Siga las instrucciones para la instalación de Dafny para su uso por terminal.
Una de las dos opciones para trabajar con repositorios remotos en GitHub usando git, es mediante el protocolo ssh junto al uso de claves públicas y privadas. Esto es completamente opcional y se puede usar otra alternativa que, quizás no tan conveniente, funciona bien y no requiere instalar herramientas extra.
En Linux/Unix o al menos las distros más conocidas, el cliente ssh viene ya instalado. Para Mac OS X, el cliente ssh también viene instalado por defecto.
En Windows 10 y 11, OpenSSH (tanto el cliente como el server) es una característica opcional que puede ser instalada fácilmente sin tener que descargar una aplicación aparte. Las instrucciones para hacerlo está en este link, se sugiere seguir las instrucciones relacionadas a la instalación mediante Windows Settings.