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 tôi có thể kiểm tra, trước khi chạy hợp đồng, các thuộc tính sau:

• Partial payments: tức là thanh toán khi không có đủ tiền trong tài khoản.

• Non positive deposits: theo đó hợp đồng yêu cầu một giá trị âm hoặc bằng không.

• Non positive payments: thanh toán bằng 0 hoặc số tiền âm.

• Shadowing of Lets, trong đó hai Letsthiế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 tôi 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 là 1Lovelace, sau đó yêu cầu Bob lựa chọn (được gọi là bool) 0hoặ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 tôi, được tích hợp trong tab MÔ PHỎNG trong Sân chơi Marlowe, 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 một khoản thanh toán 1thay vì 2.

Nếu chúng tôi 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:

Điều gì đã xảy ra

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 tôi sẽ xem xét cách trình bày kết quả phân tích của mình 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 tôi.

Sử dụng nút phân tích trong Sân chơi Marlowe để 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ể xem lý do tại sao và sửa hợp đồng để chúng không thất bại.