# Diferencias

Muestra las diferencias entre dos versiones de la página.

Enlace a la vista de comparación

materias:arquitecturas_de_software [2007/09/19 15:12]
aarbelaez
materias:arquitecturas_de_software [2011/01/24 15:30] (actual)
Línea 1: Línea 1:
+===== Arquitecturas de Software =====
+
+This web site contains information on the course **Arquitecturas de Software**, which runs on the second term 2007 at The //Pontificia Universidad Javeriana//.
+
+| **Lectures** | **Files** | **Homework** |
+|01. {{materias:lecture01-intro2fm.pdf|Introduction to Formal Methods}}| | |
+|02. {{materias:lecture02-fol-v2.pdf|First Order Logic}}| | |
+|03. {{materias:lecture03-proofsystems-v2.pdf|Proof Systems}} | | {{materias:lecture03-homework-inv-v4.pdf| Uniqueness of Inverse Element}}|
+|04. {{materias:lecture04-left-complement.pdf| A "Left Complement Example" in PVS}} | | {{materias:left_complement.dmp.gz|Left Complement}} {{materias:propositional.dmp.gz|Propositional}} |
+|05. {{materias:lecture05-phone-book.pdf| An Electronic Phone Book Example in PVS}} | {{materias:phone_book1.dmp.gz| Phone Book 1}} {{materias:phone_book2.dmp.gz| Phone Book 2}} | |
+|06. {{materias:lecture06-phone-book-v5.pdf| Sets and Invariants in PVS}} | | {{materias:lecture06-homework-lists-pvs.pdf| Lists in PVS}}|
+|07. {{materias:lecture07-bdds-v2.pdf| Modelling BDDs in PVS}} | | {{materias:lecture07-homework-bdds.pdf| BDDs in PVS}}|
+|08. {{materias:lecture08-tmis-jml-v2.pdf|An Introduction to the Java Modelling Language and Design-by-Contract}} | {{materias:decimal.tgz| Decimal class  }}|{{materias:lecture08-tmis-homework.pdf| Modeling a Stack of Integers}} |
+|10. {{materias:lecture10-thejmltool.pdf|The JML Tool}} | {{materias:purse.tgz| Purse class}}| |
+|11. {{materias:lecture11-theescjavatool.pdf|The ESC/Java 2 Tool}} | {{materias:bag.tgz| Bag}}| {{materias:lecture11-as-homework.pdf| Checking DataOutputStream}}|
+|12. Propositional Logic, Predicate Logic in Z | | |
+|13. Sets, Relations, Functions, Sequences in Z | | |
+|14. Free Types, Schemas, Preconditions in Z | | |
+|15. Data Refinement, Refinement Calculus in Z | | |
+
+===== Bibliography =====
+  * Software Reliability Methods. Doron A. Peled. Springer
+  * Model Checking. Edmund M. Clarke, Orna Grumberg and Doron A. Peled
+  * The Temporal Logic of Reactive and Concurrent Systems: Specification. Z. Manna and A. Pnueli. Springer-Verlag

materias/arquitecturas_de_software.txt · Última modificación: 2011/01/24 15:30 (editor externo)