El siguiente libro está dirigido para todas aquellas personas interesadas en aprender sobre el estándar C formalizado en Coq.
Sobre el Libro (Por el Autor)
El lenguaje de programación C fue creado por Thompson y Ritchie alrededor de 1970 como lenguaje de implementación del sistema operativo Unix.
El desarrollo de Unix demostró la eficiencia y la portabilidad de C, y luego de ese éxito, C se convirtió rápidamente en un lenguaje de programación de propósito general dominante.
Más de 40 años después de su introducción, C sigue siendo uno de los lenguajes de programación más utilizados en el mundo.
Sin embargo, a pesar de su amplio uso continuo, C también se encuentra entre los lenguajes de programación más propensos a errores en el mundo.
Como resultado de la escritura estática débil y la ausencia de controles en tiempo de ejecución, es muy fácil que los programas C tengan errores que hagan que el programa se bloquee o se comporte mal de otras formas.
Los punteros colgantes y los punteros NULL se pueden desreferenciar, se puede acceder a las matrices fuera de sus límites, etc.
Un ejemplo reciente es el error Heartbleed en la biblioteca de criptografía OpenSSL ampliamente utilizada, donde un desbordamiento de búfer permitió el acceso a datos arbitrarios, que pueden contener contraseñas.
Heartbleed no es un caso incidental donde la inseguridad de C tiene consecuencias desastrosas. Wang et al. han demostrado que la inseguridad de C es un problema grave.
En lenguajes de programación más seguros que C, es menos probable que ocurran errores como estos, pero debido a los beneficios de rendimiento, control y portabilidad de C, el uso de C y derivados de C como C++ sigue siendo generalizado.
La verificación formal es un enfoque prometedor para conservar los beneficios de rendimiento, control y portabilidad de C pero sin los peligros de su inseguridad. En la verificación formal, se utilizan métodos matemáticos para obtener el nivel más alto de garantía de la seguridad de un programa, o incluso de toda su corrección funcional.
Contenido (Temas)
- Contenido
- Expresiones de gratitud
- Introducción
- Sutilezas de C
- Tipos en C
- Permisos y álgebras de separación
- El modelo de la memoria
- CH2O núcleo C
- CH2O resumen C
- Lógica de separación
- Formalización en Coq
- Trabajo relacionado
- Conclusión y trabajo futuro
- Bibliografía
- Sintaxis
- Resumen
- Samenvatting
- Plan de estudios VI
Ficha Técnica
Año: 2015
Editor: Radbound University
Idioma: Inglés
Tamaño: 1655 KB
Licencia: Pendiente de revisión
Acerca de OpenLibra
OpenLibra busca reunir bajo una misma plataforma el mayor número de publicaciones libres posible. Esto implica una serie de riesgos en cuanto a los contenidos que han de asumirse y sobre los que queremos informar a nuestros usuarios.
En OpenLibra, los libros son responsabilidad exclusiva de sus autores. Esto significa que OpenLibra, no puede garantizar la validez de sus contenidos.
Te Puede Interesar
- 6 Libros Gratis para Aprender CSS
- El Departamento de Ciencias de la Computación de Stanford te da este PDF Gratis del Lenguaje C
- 5 Libros Gratis en Español de Sistemas Operativos
- La Universitat Jaume I te da este PDF Gratis de Educación inclusiva
- PDF Gratis de Diseño y Desarrollo de un Videojuego no Euclídeo por la Universidad Complutense de Madrid
- Un primer Curso de Álgebra Lineal – PDF Gratis
- Conoce las Tendencias Universidad con este PDF Gratis Ofrecido por la UNESCO
- Conviértete en Experto de la Astronomía con este Astrodiccionario
- PDF Gratis de Filosofía de las Ciencias Sociales
- PDF Gratis del Lenguaje de Programación C formalizado en Coq
Preguntas Frecuentes
¿Qué quiere decir Biblioteca Libre?
Quiere decir que todos los libros que la componen están licenciados bajo alguno de los muchos tipos de licencia libre que existen y que, por tanto, el autor da su autorización para su reproducción y redistribución.
¿Son entonces todos los libros de esta biblioteca gratis?
Sí; al menos para su versión digital. Muchos autores, además, ofrecen la versión impresa (ya sea directamente o a través del circuito comercial habitual) por la que pueden cobrar lo que estimen oportuno.
Pero algunos de los libros que hay en la Biblioteca tienen Copyright…
El copyright y las licencias libres no son excluyentes. De hecho, las segundas se basan en la legislación sobre la primera para otorgar los derechos de copia y distribución. Es por eso que toda obra bajo una licencia libre, posee un copyright que garantiza la voluntad de su autor. Lo importante es qué permite ese copyright con respecto a la obra licenciada.
Pues he visto algún libro por aquí que tiene un Copyright y un ‘todos los derechos reservados’.
Cierto; en estos casos, lo más habitual es que la editorial haya devuelto los derechos de explotación al autor. Suele ocurrir con los manuales técnicos una vez pasado un tiempo prudencial o, por ejemplo, cuando se han agotado las ediciones impresas y no se pretende una reedición. Una vez los autores vuelven a tener el control, pueden ceder su trabajo al dominio público o permitir su redistribución libre para volver a poner su obra en circulación.
Si los libros son libres y gratis, ¿puedo hacer con ellos lo que quiera? ¿Los puedo imprimir, traducir y/o vender?
No; no puedes hacer aquello que su licencia no permita. Cómo se explica en el enlace de más arriba, algunas licencias solo permiten la descarga y redistribución sin ánimo de lucro. Si por ejemplo, quieres traducir la obra y editarla de forma ordinaria, algunos autores te exigirán que pagues los derechos pertinentes.
Descarga el Libro
Si te interesaron los temas, te dejamos aquí abajo el enlace de descarga.
¿Quieres Más?
Encuentra cursos y libros gratuitos, además de cupones de Udemy, en nuestros Telegram.
