Nội dung được dịch bởi AI, chỉ mang tính chất tham khảo
Logic phân tách: một logic cho cấu trúc dữ liệu có thể biến đổi chia sẻ
Proceedings - Symposium on Logic in Computer Science - Trang 55-74
Tóm tắt
Trong công trình hợp tác với Peter O'Hearn và những người khác, dựa trên những ý tưởng ban đầu của Burstall, chúng tôi đã phát triển một mở rộng của logic Hoare cho phép lập luận về các chương trình lệnh cấp thấp sử dụng cấu trúc dữ liệu có thể thay đổi được chia sẻ. Ngôn ngữ lập trình lệnh đơn giản được mở rộng với các lệnh (không phải biểu thức) để truy cập và sửa đổi các cấu trúc chia sẻ, cũng như cho việc cấp phát và giải phóng bộ nhớ một cách rõ ràng. Các khẳng định được mở rộng bằng cách giới thiệu một "phép kết hợp phân tách" xác nhận rằng các công thức con của nó đúng cho các phần không giao nhau của heap, cùng với một "suy diễn phân tách" có liên quan chặt chẽ. Kết hợp với định nghĩa quy nạp của các định đề trên các cấu trúc dữ liệu trừu tượng, sự mở rộng này cho phép mô tả ngắn gọn và linh hoạt các cấu trúc với việc chia sẻ được kiểm soát. Trong bài báo này, chúng tôi khảo sát sự phát triển hiện tại của logic chương trình này, bao gồm những mở rộng cho phép số học địa chỉ không bị hạn chế, các mảng được cấp phát động và các quy trình đệ quy. Chúng tôi cũng thảo luận về những hướng đi hứa hẹn trong tương lai.
Từ khóa
#Data structures #Computer science #Programmable logic arrays #Reflection #Logic programming #Computer languages #Logic arrays #Arithmetic #Artificial intelligence #BibliographiesTài liệu tham khảo
10.1145/360204.375719
yang, 2002, A semantic basis for local reasoning, Lecture Notes in Computer Science, 2303, 402, 10.1007/3-540-45931-6_28
10.1145/362452.362489
10.1007/978-1-4757-3472-0_6
yang, 2001, An example of local reasoning in BI pointer logic: The Schorr-Waite graph marking algorithm, SPACE 2001 Informal Proceedings of Workshop on Semantics Program Analysis and Computing Environments for Memory Management, 41
harel, 2000, Dynamic Logic, 10.7551/mitpress/2516.001.0001
yang, 2001, Local Reasoning for Stateful Programs
10.1145/363235.363259
10.1007/3-540-45500-0_13
10.1007/3-540-45793-3_13
10.1145/325694.325742
conforti, 2002, The query language TQL, Proc Workshop Web and Databases (WebDB)
o'hearn, 2001, Notes on conditional critical regions in spatial pointer logic
morrisett, 1998, Stack-based typed assembly language, Lecture Notes in Computer Science, 1473, 28, 10.1007/BFb0055511
o'hearn, 2002, Notes on separation logic for shared-variable concurrency
10.2307/421090
o'hearn, 2001, Local reasoning about programs that alter data structures, Lecture Notes in Computer Science, 2142, 1, 10.1007/3-540-44802-0_1
10.1145/360051.360224
pym, 2002, The Semantics and Proof Theory of the Logic of Bunched Implications, 10.1007/978-94-017-0091-7
reynolds, 1981, The Crafi of Programming
reynolds, 2000, Intuitionistic reasoning about shared mutable data structure, Millennial Perspectives in Computer Science, 303
reynolds, 2000, Lectures on reasoning about shared mutable data structure
caires, 1998, Verifiable and executable specifications of concurrent objects in L?, Lecture Notes in Computer Science, 1381, 42, 10.1007/BFb0053562
burstall, 1972, Some techniques for proving correctness of programs which alter data structures, Machine Intelligence, 7, 23
cardelli, 2001, A query language based on the ambient logic, Lecture Notes in Computer Science, 2028, 1, 10.1007/3-540-45309-1_1
bornat, 2001, Explicit description in BI pointer logic
reynolds, 2001, Reasoning about shared mutable data structure (abstract of invited lecture), SPACE 2001 Informal Proceedings of Workshop on Semantics Program Analysis and Computing Environments for Memory Management, 7
calcagno, 2001, Program logic and equivalence in the presence of garbage collection
calcagno, 2001, On garbage and program logic, Lecture Notes in Computer Science, 2030, 137, 10.1007/3-540-45315-6_9
10.1007/3-540-45332-6_7
calcagno, 2002, Semantic and Logical Properties of Stateful Programmming
tofte, 1994, Implementation of the typed call-by-value ?-calculus using a stack of regions, Conference Record of POPL '97 The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 188, 10.1145/174675.177855
calcagno, 2001, Program logics in the presence of garbage collection (abstract), SPACE 2001 Informal Proceedings of Workshop on Semantics Program Analysis and Computing Environments for Memory Management, 11
cardelli, 2002, A spatial logic for querying graphs, Automata Languages and Programming
calcagno, 2001, Computability and complexity results for a spatial assertion language for data structures, Lecture Notes in Computer Science, 108, 10.1007/3-540-45294-X_10