Contribuciones del usuario
Para Mjoseh (discusión | registro de bloqueos | subidas | registros)(últimas | primeras) Ver (50 siguientes | 50 anteriores) (20 | 50 | 100 | 250 | 500).
- 11:22 11 oct 2016 (dif | hist) . . (+27) . . Tema 12: Definiciones inductivas en Isabelle/HOL. Caso de estudio: clausura reflexiva transitiva.
- 10:20 31 mar 2016 (dif | hist) . . (+3197) . . N Rel 12 (Página creada con '<source lang = "Isar"> theory Hoare_anotado_ejercicios imports "VCG_b" "Hoare_Total_b" begin definition "MUL ≡ ''z''::=N 0;; ''c''::=N 0;; WHILE (Less (V ...') (edición actual)
- 10:19 31 mar 2016 (dif | hist) . . (+3196) . . N Rel 12 (e) (Página creada con '<source lang = "Isar"> theory Hoare_anotado_ejercicios imports "VCG_b" "Hoare_Total_b" begin definition "MUL ≡ ''z''::=N 0;; ''c''::=N 0;; WHILE (Less (V ...')
- 10:18 31 mar 2016 (dif | hist) . . (+4088) . . N Rel 11 (Página creada con '<source lang = "Isar"> theory Hoare_ejercicios_1 imports "Hoare_b_ejemplos" "Hoare_Sound_Complete_b" begin text{* Ejercicio 1: Definir una función bsubst fun bsubst :: "be...') (edición actual)
- 10:18 31 mar 2016 (dif | hist) . . (0) . . m Rel 11 (e) (Protegió «Rel 11 (e)» ([edit=sysop] (indefinido) [move=sysop] (indefinido)))
- 10:18 31 mar 2016 (dif | hist) . . (+4087) . . N Rel 11 (e) (Página creada con '<source lang = "Isar"> theory Hoare_ejercicios_1 imports "Hoare_b_ejemplos" "Hoare_Sound_Complete_b" begin text{* Ejercicio 1: Definir una función bsubst fun bsubst :: "be...')
- 10:17 31 mar 2016 (dif | hist) . . (+386) . . Ejercicios
- 14:49 25 feb 2016 (dif | hist) . . (-234) . . Temas (edición actual)
- 10:41 9 feb 2016 (dif | hist) . . (0) . . Tema 17: Lógica de Hoare en Isabelle/HOL. (edición actual)
- 20:14 8 feb 2016 (dif | hist) . . (+6871) . . N Tema 20: Lógica de Hoare en Isabelle/HOL: condiciones de verificación. (Página creada con '<source lang = "Isar"> header "Condiciones de verificación" theory VCG_b imports Hoare_b begin text{* Condiciones de verificación: El objetivo es transformar la noción de ...') (edición actual)
- 20:13 8 feb 2016 (dif | hist) . . (+9397) . . N Tema 19: Lógica de Hoare en Isabelle/HOL: adecuación y completitud de la corrección total. (Página creada con '<source lang = "Isar"> theory Hoare_Total_b imports Hoare_Sound_Complete_b begin text{* Lógica de Hoare: corrección total. *} text{* La noción informal de corrección tota...') (edición actual)
- 20:12 8 feb 2016 (dif | hist) . . (+297) . . Temas LCyTM 2015 (edición actual)
- 21:13 2 feb 2016 (dif | hist) . . (+4715) . . N Ejemplos de verificación de propiedades en Lógica de Hoare usando Isabelle/HOL. (Página creada con '<source lang = "Isar"> theory Hoare_b_ejemplos imports "Hoare_b" begin text{* Ejemplo 1: programa que calcula el máximo de a y b, y lo guarda en c. *} definition MAX :: com...') (edición actual)
- 21:12 2 feb 2016 (dif | hist) . . (+154) . . Temas LCyTM 2015
- 14:21 2 feb 2016 (dif | hist) . . (+1) . . Tema 18: Adecuación y completitud de la Lógica de Hoare en Isabelle/HOL. (edición actual)
- 14:21 2 feb 2016 (dif | hist) . . (+5246) . . N Tema 18: Adecuación y completitud de la Lógica de Hoare en Isabelle/HOL. (Página creada con '<source lang = Isar"> theory Hoare_Sound_Complete_b imports Hoare_b begin text{* Teorema de adecuación de la Lógica de Hoare con respecto a la semántica operacional: si ...')
- 14:20 2 feb 2016 (dif | hist) . . (+153) . . Temas LCyTM 2015
- 11:27 1 feb 2016 (dif | hist) . . (+472) . . Tema 17: Lógica de Hoare en Isabelle/HOL.
- 13:31 26 ene 2016 (dif | hist) . . (0) . . Tema 17: Lógica de Hoare en Isabelle/HOL.
- 13:31 26 ene 2016 (dif | hist) . . (0) . . Tema 17: Lógica de Hoare en Isabelle/HOL.
- 13:30 26 ene 2016 (dif | hist) . . (+8121) . . N Tema 17: Lógica de Hoare en Isabelle/HOL. (Página creada con '<source land = "isar"> header "Hoare Logic" theory Hoare_b imports Big_Step_b begin text{* La Lógica de Hoare (creada por Tony Hoare) es una lógica para probar propiedades ...')
- 13:30 26 ene 2016 (dif | hist) . . (+106) . . Temas LCyTM 2015
- 13:34 21 ene 2016 (dif | hist) . . (+278) . . Rel 9
- 11:45 20 ene 2016 (dif | hist) . . (0) . . m Tema 16: Semántica operacional del lenguaje imperativo simple IMP. (Protegió «Tema 16: Semántica operacional del lenguaje imperativo simple IMP.» ([edit=sysop] (indefinido) [move=sysop] (indefinido))) (edición actual)
- 11:45 20 ene 2016 (dif | hist) . . (0) . . m Rel 9 (e) (Protegió «Rel 9 (e)» ([edit=sysop] (indefinido) [move=sysop] (indefinido)))
- 11:45 20 ene 2016 (dif | hist) . . (0) . . m Rel 8 (e) (Protegió «Rel 8 (e)» ([edit=sysop] (indefinido) [move=sysop] (indefinido)))
- 11:44 20 ene 2016 (dif | hist) . . (+3103) . . N Rel 10 (Página creada con '<source lang = "isar"> theory Big_Step_ejercicios imports Big_Step_b begin text{* Ejercicios *} text{* Ejercicio 1.1 Definir una función fun assigned :: "com ⇒ vname ...')
- 11:44 20 ene 2016 (dif | hist) . . (0) . . m Rel 10 (e) (Protegió «Rel 10 (e)» ([edit=sysop] (indefinido) [move=sysop] (indefinido)))
- 11:44 20 ene 2016 (dif | hist) . . (+3103) . . N Rel 10 (e) (Página creada con '<source lang = "isar"> theory Big_Step_ejercicios imports Big_Step_b begin text{* Ejercicios *} text{* Ejercicio 1.1 Definir una función fun assigned :: "com ⇒ vname ...')
- 11:43 20 ene 2016 (dif | hist) . . (+200) . . Ejercicios
- 11:40 20 ene 2016 (dif | hist) . . (+15 045) . . N Tema 16: Semántica operacional del lenguaje imperativo simple IMP. (Página creada con '<source lang = "isar"> theory Big_Step_b imports Com_b begin subsection "Semántica de paso largo." text{* En esta sección definimos una semántica operacional para dar sign...')
- 11:39 20 ene 2016 (dif | hist) . . (+134) . . Temas LCyTM 2015
- 12:28 15 ene 2016 (dif | hist) . . (-25) . . Tema 15: Sintaxis de un lenguaje imperativo simple. (edición actual)
- 11:55 13 ene 2016 (dif | hist) . . (+1663) . . N Tema 15: Sintaxis de un lenguaje imperativo simple. (Página creada con '<source lang = "isar"> header "IMP: sintaxis de un lenguaje imperativo simple" theory Com_b imports BExp_b begin text{* Definimos un lenguaje imperativo con las instrucciones ...')
- 11:55 13 ene 2016 (dif | hist) . . (+113) . . Temas LCyTM 2015
- 10:20 13 ene 2016 (dif | hist) . . (+6) . . Temas LCyTM 2015
- 10:14 13 ene 2016 (dif | hist) . . (+9514) . . N Rel 9 (Página creada con '<source lang = "isar"> header "Ejercicios sobre expresiones booleanas" theory BExp_ejercicios imports AExp_b BExp_b begin text{* Ejercicios text{* Ejercicio 1.1. Defin...')
- 10:13 13 ene 2016 (dif | hist) . . (+9512) . . N Rel 9 (e) (Página creada con '<source lang = "isar"> header "Ejercicios sobre expresiones booleanas" theory BExp_ejercicios imports AExp_b BExp_b begin text{* Ejercicios text{* Ejercicio 1.1. Defini...')
- 10:12 13 ene 2016 (dif | hist) . . (+185) . . Ejercicios
- 10:11 13 ene 2016 (dif | hist) . . (+3584) . . N Tema 14: Expresiones booleanas. (Página creada con '<source lang = "isar"> theory BExp_b imports AExp_b begin subsection "Expresiones booleanas" text{* Una expresión booleana es: - una constante booleana, o - la negación ...') (edición actual)
- 09:08 7 ene 2016 (dif | hist) . . (-5) . . Ejercicios
- 09:04 7 ene 2016 (dif | hist) . . (+11) . . Ejercicios
- 23:16 6 ene 2016 (dif | hist) . . (+6583) . . N Rel 8 (Página creada con '<source lang = "isar"> header "Ejercicios sobre expresiones aritméticas" theory AExp_ejercicios imports AExp_b begin text{* Ejercicios Ejercicio 1.1. Para probar que la ...')
- 23:14 6 ene 2016 (dif | hist) . . (+6581) . . N Rel 8 (e) (Página creada con '<source lang = "isar"> header "Ejercicios sobre expresiones aritméticas" theory AExp_ejercicios imports AExp_b begin text{* Ejercicios Ejercicio 1.1. Para probar que la f...')
- 23:13 6 ene 2016 (dif | hist) . . (+7) . . Ejercicios
- 23:12 6 ene 2016 (dif | hist) . . (+174) . . Ejercicios
- 23:08 6 ene 2016 (dif | hist) . . (+5268) . . Tema 13: Expresiones aritméticas. (edición actual)
- 13:31 5 ene 2016 (dif | hist) . . (-15) . . Temas
- 13:31 5 ene 2016 (dif | hist) . . (+16) . . Temas
- 13:30 5 ene 2016 (dif | hist) . . (+223) . . Temas
(últimas | primeras) Ver (50 siguientes | 50 anteriores) (20 | 50 | 100 | 250 | 500).