Bài 11: Phân tích tĩnh

Một tính năng đặc biệt của Marlowe - có lẽ là tính năng đặc biệt nhất của nó - là chúng ta có thể phân tích các hợp đồng và suy ra các thuộc tính của chúng mà không cần chạy chúng.

chúng ta có thể kiểm tra, trước khi chạy hợp đồng, các thuộc tính sau:

• Thanh toán từng phần: tức là thanh toán khi không có đủ tiền trong tài khoản.
• Tiền gửi âm (<0): theo đó hợp đồng yêu cầu một giá trị âm hoặc bằng không.
• Thanh toán âm (<0): thanh toán bằng 0 hoặc số tiền âm.
• Shadowing of Lets, trong đó hai Lets thiết lập cùng một số nhận dạng trong cùng một đường dẫn thực thi.

Trong phần còn lại của hướng dẫn này, chúng ta sẽ tập trung vào lỗi đầu tiên, đây là loại lỗi nặng nhất. Đó là trong trường hợp thanh toán không thành công, bởi vì không có đủ tiền trong hợp đồng (hoặc nghiêm ngặt hơn trong tài khoản) để thực hiện một khoản thanh toán hoàn chỉnh.

Một ví dụ

Chúng ta hãy xem ví dụ này, trong Blockly

và trong Marlowe thuần túy

Trước tiên, hợp đồng yêu cầu một khoản tiền gửi từ Alice of 1 Lovelace, sau đó yêu cầu Bob lựa chọn (được gọi là bool) 0 hoặc 1. Sau đó, hợp đồng thanh toán lựa chọn này cộng với một lựa chọn cho Bob từ tài khoản của Alice.

Vì vậy, chúng ta có thể thấy rằng mặc dù hợp đồng có hiệu lực khi Bob chọn 0, nhưng sẽ không có đủ trong hợp đồng để trả cho anh ta nếu anh ta chọn 1. Phân tích của chúng ta, được tích hợp trong tab MÔ PHỎNG trong Marlowe Playground, có thể chẩn đoán điều này:

Điều này cho thấy rằng lỗi xảy ra khi

• Alice đã gửi tiền và
• Bob đã chọn giá trị 1.

và lỗi được tạo ra là TransactionPartialPay: trong trường hợp này Bob chỉ nhận được khoản thanh toán 1 thay vì 2.

Nếu chúng ta sửa đổi hợp đồng để Alice đặt cược ban đầu 2, thì phân tích - lần này được gọi từ chế độ xem Blockly - sẽ thành công:

Bảo trì

Chỉ để lặp lại: tác dụng của phân tích này là kiểm tra mọi đường dẫn thực hiện có thể có thông qua hợp đồng, sử dụng phiên bản tượng trưng của hợp đồng. Điều này được chuyển đến bộ giải Z3 SMT, đây là một hệ thống tự động hiện đại để quyết định xem các công thức logic có thỏa mãn hay không.

Nếu phân tích không thành công, tức là nếu có một cách nào đó khiến hợp đồng không thanh toán được, thì hệ thống cũng sẽ đưa ra một ví dụ về cách nó có thể xảy ra sai sót và trình bày điều đó cho người dùng. Sau đó, người dùng có thể khắc phục sự cố và kiểm tra lại.

Bước tiếp theo

Trong vài tháng tới, chúng ta sẽ xem xét cách trình bày kết quả phân tích của chúng ta theo cách “thân thiện với người dùng” hơn, cũng như mở rộng phạm vi công việc của chúng ta.

Sử dụng node phân tích trong Marlowe Playground để phân tích một số hợp đồng mà bạn đã viết. Nếu phân tích không thành công, bạn có thể thấy lý do tại sao và sửa hợp đồng để chúng không thất bại.

---