Tipp
Weitere Kapitel dieses Buchs durch Wischen aufrufen
Tipp schließen
Apply-scripts are unreadable and hard to maintain. The language of choice for larger proofs is Isar. The two key features of Isar are (1) It is structured, not linear. (2) It is readable without its being run because you need to state what you are proving at any given point. Whereas apply-scripts are like assembly language programs, Isar proofs are like structured programs with comments. A typical Isar proof looks like this.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten
Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:
Springer Professional "Wirtschaft+Technik"
Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:
über 69.000 Bücher
über 500 Zeitschriften
aus folgenden Fachgebieten:
Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Umwelt
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko
Testen Sie jetzt 30 Tage kostenlos.
Springer Professional "Technik"
Mit Springer Professional "Technik" erhalten Sie Zugriff auf:
über 50.000 Bücher
über 380 Zeitschriften
aus folgenden Fachgebieten:
Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Umwelt
Maschinenbau + Werkstoffe
Testen Sie jetzt 30 Tage kostenlos.
Springer Professional "Wirtschaft"
Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:
über 58.000 Bücher
über 300 Zeitschriften
aus folgenden Fachgebieten:
Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko
Testen Sie jetzt 30 Tage kostenlos.
Titel
Isar: a Language for Structured Proofs
Buch
Concrete Semantics
Print ISBN: 978-3-319-10541-3
Electronic ISBN: 978-3-319-10542-0
Copyright-Jahr: 2014
https://doi.org/10.1007/978-3-319-10542-0
DOI
https://doi.org/10.1007/978-3-319-10542-0_5
Autoren:
Tobias Nipkow
Sequenznummer
5
Kapitelnummer
Chapter 5
