Hacktoberfest 2026: những issue maintainer đã đánh dấu cho tháng Mười, đang mở và phù hợp người mới. Xem issue Hacktoberfest

[Bug] Incorrect online execution result in SPARK tutorial (2/2)

Đang mở
  • Có gì không ổn?
#718 1 bình luận 0 reaction 0 người được giao Xem trên GitHub

Chưa có ai nhận issue này.

Đánh giá

Độ khó
3/5
Thời gian dự kiến
1-2 ngày
Mức phù hợp với người mới
35/100
Loại issue
Lỗi
Độ rõ ràng
Khá rõ ràng
Mức độ hoạt động
Đình trệ
Lĩnh vực
documentation

Hướng nghiên cứu

Bắt đầu với Example_08 trong Courses.Intro_To_Spark.Proof_of_Functional_Correctness và so sánh playground trực tuyến với việc thực thi cục bộ array_util.adb sau khi di chuyển L7-L8. Chạy lệnh gnatprove được nêu và kiểm tra đầu ra của playground; được xem là hoàn tất khi các kết quả trực tuyến và cục bộ nhất quán xác định lỗi ngữ nghĩa.

Do mô hình lập chỉ mục viết ra từ nội dung của issue.

Mô tả

In Courses.Intro_To_Spark.Proof_of_Functional_Correctness.Example_08:

I tried moving L7-L8 in array_util.adb to the end of if-else which should be an obvious semantic error to be fixed.

However, the online playground complains:

image

Local execution, on the other hand, completes without any problem:

> gnatprove -P main.gpr --checks-as-errors --level=0 --no-axiom-guard --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...

main.adb:6:30: warning: array aggregate using () is an obsolescent syntax, use [] instead [-gnatwj]
    6 |   A : constant Nat_Array := (1, 1, 2);
      |                             ^~~~~~~~

main.adb:7:30: warning: array aggregate using () is an obsolescent syntax, use [] instead [-gnatwj]
    7 |   B : constant Nat_Array := (2, 1, 0);
      |                             ^~~~~~~~

main.adb:8:04: warning: constant "R" is not referenced [-gnatwu]
    8 |   R : constant Nat_Array (1..3) := Max_Array (A, B);
      |   ^ here
array_util.adb:6:07: info: range check proved
array_util.adb:6:34: info: length check proved
array_util.adb:10:24: info: index check proved
array_util.adb:13:25: info: index check proved
array_util.adb:15:33: info: loop invariant preservation proved
array_util.adb:15:33: info: loop invariant initialization proved
array_util.adb:16:40: info: index check proved
array_util.adb:16:61: info: index check proved
array_util.adb:16:68: info: index check proved
array_util.ads:9:14: info: postcondition proved
array_util.ads:10:34: info: index check proved
array_util.ads:10:55: info: index check proved
array_util.ads:10:62: info: index check proved

> gnatprove --version
SPARK Pro 23.0w (20220412)
Why3 for gnatprove version 1.4.1+git
alt-ergo: Alt-Ergo version 2.4.0
colibri: Colibri 2020.9
cvc4: This is CVC4 version 1.8
z3: Z3 version 4.8.15 - 64 bit
Ngôn ngữ chính
Ada
Star
117
Fork
50
Merge trung bình
5 giờ 1 phút
Pull request đã merge (30 ngày)
2

Chuẩn bị môi trường

Bắt đầu từ đâu

  1. Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
  2. Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
  3. Fork repository và làm thay đổi trên một nhánh.
  4. Mở pull request có tham chiếu số hiệu của issue.

Issue khác của AdaCore/learn

Tất cả issue của AdaCore/learn

Issue tương tự

Thêm issue về Documentation

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.