Kinh doanh - Marketing
Kinh tế quản lý
Biểu mẫu - Văn bản
Tài chính - Ngân hàng
Công nghệ thông tin
Tiếng anh ngoại ngữ
Kĩ thuật công nghệ
Khoa học tự nhiên
Khoa học xã hội
Văn hóa nghệ thuật
Sức khỏe - Y tế
Văn bản luật
Nông Lâm Ngư
Kỹ năng mềm
Luận văn - Báo cáo
Giải trí - Thư giãn
Tài liệu phổ thông
Văn mẫu
Giới thiệu
Đăng ký
Đăng nhập
Tìm
Danh mục
Kinh doanh - Marketing
Kinh tế quản lý
Biểu mẫu - Văn bản
Tài chính - Ngân hàng
Công nghệ thông tin
Tiếng anh ngoại ngữ
Kĩ thuật công nghệ
Khoa học tự nhiên
Khoa học xã hội
Văn hóa nghệ thuật
Y tế sức khỏe
Văn bản luật
Nông lâm ngư
Kĩ năng mềm
Luận văn - Báo cáo
Giải trí - Thư giãn
Tài liệu phổ thông
Văn mẫu
Thông tin
Điều khoản sử dụng
Quy định bảo mật
Quy chế hoạt động
Chính sách bản quyền
Giới thiệu
Đăng ký
Đăng nhập
0
Trang chủ
Công Nghệ Thông Tin
Kỹ thuật lập trình
Lecture Programming languages (2/e): Chapter 18a - Tucker, Noonan
Đang chuẩn bị liên kết để tải về tài liệu:
Lecture Programming languages (2/e): Chapter 18a - Tucker, Noonan
Thúy Vy
48
19
ppt
Đang chuẩn bị nút TẢI XUỐNG, xin hãy chờ
Tải xuống
Chapter 18 - Program correctness. This chapter provides knowledge of axiomatic semantics. This chapter includes contents: Fundamental concepts, the assignment rule, rules of consequence, correctness of the max function, correctness of programs with loops. | Programming Languages 2nd edition Tucker and Noonan Chapter 18 Program Correctness To treat programming scientifically, it must be possible to specify the required properties of programs precisely. Formality is certainly not an end in itself. The importance of formal specifications must ultimately rest in their utility - in whether or not they are used to improve the quality of software or to reduce the cost of producing and maintaining software. J. Horning Contents 18.1 Axiomatic Semantics 18.1.1 Fundamental Concepts 18.1.2 The Assignment Rule 18.1.3 Rules of Consequence 18.1.4 Correctness of the Max Function 18.1.5 Correctness of Programs with Loops 18.2 Formal Methods Tools: JML 18.3 Correctness of Object-Oriented Programs 18.4 Correctness of Functional Programs Motivation A correct program is one that does exactly what it is intended to do, no more and no less. A formally correct program is one whose correctness can be proved mathematically. This requires a language for specifying precisely what the program is intended to do. Specification languages are based in mathematical logic. Hoare invented “axiomatic semantics” in 1969 as a tool for specifying program behavior and proving correctness. Until recently, correctness has been an academic exercise. Now it is a key element of critical software systems. Correctness Tools Theorem provers PVS Modeling languages UML and OCL Specification languages JML Programming language support Eiffel Java Spark/Ada Specification Methodology Design by contract 18.1 Axiomatic Semantics Axiomatic semantics is a language for specifying what a program is supposed to do. Based on the idea of an assertion: An assertion is a predicate that describes the state of a program at a point in its execution. A postcondition is an assertion that states the program’s result. A precondition is an assertion that states what must be true before the program begins running. A “Hoare Triple” has the form {P}s{Q} {true} int Max (int a, int b) { int m; . | Programming Languages 2nd edition Tucker and Noonan Chapter 18 Program Correctness To treat programming scientifically, it must be possible to specify the required properties of programs precisely. Formality is certainly not an end in itself. The importance of formal specifications must ultimately rest in their utility - in whether or not they are used to improve the quality of software or to reduce the cost of producing and maintaining software. J. Horning Contents 18.1 Axiomatic Semantics 18.1.1 Fundamental Concepts 18.1.2 The Assignment Rule 18.1.3 Rules of Consequence 18.1.4 Correctness of the Max Function 18.1.5 Correctness of Programs with Loops 18.2 Formal Methods Tools: JML 18.3 Correctness of Object-Oriented Programs 18.4 Correctness of Functional Programs Motivation A correct program is one that does exactly what it is intended to do, no more and no less. A formally correct program is one whose correctness can be proved mathematically. This requires a language for specifying
TÀI LIỆU LIÊN QUAN
Lecture Programming languages (2/e): Chapter 12b - Tucker, Noonan
Lecture Programming languages (2/e): Chapter 14a - Tucker, Noonan
Lecture Programming languages (2/e): Chapter 15a - Tucker, Noonan
Lecture Programming languages (2/e): Chapter 12d - Tucker, Noonan
Lecture Introduction to computing - Lesson 19: Programming languages
Lecture Programming languages (2/e): Chapter 12a - Tucker, Noonan
Lecture Programming languages (2/e): Chapter 12c - Tucker, Noonan
Lecture Programming languages (2/e): Chapter 13a - Tucker, Noonan
Lecture Programming languages (2/e): Chapter 13b - Tucker, Noonan
Lecture Programming languages (2/e): Chapter 13c - Tucker, Noonan
crossorigin="anonymous">
Đã phát hiện trình chặn quảng cáo AdBlock
Trang web này phụ thuộc vào doanh thu từ số lần hiển thị quảng cáo để tồn tại. Vui lòng tắt trình chặn quảng cáo của bạn hoặc tạm dừng tính năng chặn quảng cáo cho trang web này.