External specs: a @StateSet declared later in the file is not found by an interface earlier in it

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

Maintainer thường phản hồi trong vòng 2 ngày

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

Đánh giá

Độ khó
4/5
Thời gian dự kiến
3-5 ngày
Mức phù hợp với người mới
58/100
Loại issue
Lỗi
Độ rõ ràng
Đặc tả rõ ràng
Mức độ hoạt động
Sôi nổi
Công nghệ
java
Lĩnh vực
compilers, testing-qa

Hướng nghiên cứu

Start with the verifier code that resolves @StateSet declarations and the V32_StateSetDeclaredLater probe in liquid-java/co-specification. Trace why a state declared in a later external refinement interface is unavailable to an earlier interface, then run the probe before and after the change. Done means the reproducer verifies successfully regardless of declaration order.

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

Mô tả

When one spec file holds external refinements for several classes of a hierarchy, the interface that declares the @StateSet has to come first in the file. If an interface earlier in the file uses the states, verification fails with Not Found Error: Ghost '...' could not be found, even though the declaration is in the same file. Declaration order should not matter.

Minimal reproducer

FrameRefinements.java:

import liquidjava.specification.ExternalRefinementsFor;
import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;

@ExternalRefinementsFor("java.awt.Frame")
public interface FrameRefinements {
    @StateRefinement(to = "notDisplayable(this)")
    void Frame();

    @StateRefinement(from = "notDisplayable(this)")
    void setUndecorated(boolean undecorated);
}

@ExternalRefinementsFor("java.awt.Window")
@StateSet({"notDisplayable", "displayable"})     // declared here, after its first use above
interface WindowRefinements {
    @StateRefinement(to = "displayable(this)")
    void pack();
}

Client.java (correct code):

import java.awt.Frame;

public class Client {
    public static void main(String[] args) {
        Frame f = new Frame();
        f.setUndecorated(true);
        f.pack();
    }
}

Found:

Not Found Error: Ghost 'java.awt.Frame.notDisplayable' could not be found
    @StateRefinement(to = "notDisplayable(this)")

Expected: Correct! Passed Verification., as when the WindowRefinements interface is moved above FrameRefinements (nothing else changed).

Real-world scenario

Frame.setUndecorated throws IllegalComponentStateException: The frame is displayable. once the frame has a peer, and pack()/setVisible(true) (declared in java.awt.Window) create it. A spec for this, used to catch real bugs like calling setUndecorated(true) after pack() in a game window, needs interfaces for Window, Frame, Component and JFrame. The state must be declared on Window, since a state declared on Frame cannot be used by Window.pack() (expected Frame, got Window, which seems right). The natural order, with the class being specified first, then fails as above.

Verifier commit 1a506fe. Reproducer as a verifier probe: liquid-java/co-specification verifier-probes/V32_StateSetDeclaredLater.

Ngôn ngữ chính
Java
Star
71
Fork
37
Merge trung bình
1 ngày 19 giờ
Pull request đã merge (30 ngày)
46

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 liquid-java/liquidjava

Tất cả issue của liquid-java/liquidjava

Issue tương tự

Thêm issue về Java

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.