Description

CatarinaGamboa

opened on Sep 24, 2026

Issue body actions

Alias expansion is used when checking a refinement, but the current VC simplification history does not record it. The earlier alias derivation feature from #160 and #184 was removed during the migration to VC simplification in #261.

For example, E_A2_04_CsvChunker reports Expected: Positive(buffered), Found: Nat(buffered), and counterexample buffered == 0. Here Nat(x) means x >= 0 and Positive(x) means x > 0, but the diagnostic contains no step that reveals those definitions.

Preserve the alias expansions used in a failed check as structured diagnostic data for both the found and expected refinements. A client should be able to show the substituted definitions and navigate back to the alias names. Add a regression test for this example or an equivalent mismatch.

Activity

1. CatarinaGamboa

   added

   studyNeeded before the error-message user studyNeeded before the error-message user study

   on Nov 5, 2026
2. CatarinaGamboa commented on Nov 5, 2026

   

   CatarinaGamboa

   on Nov 5, 2026

   CollaboratorAuthor

   More actions

   Labelled study: the error-message study's specs use aliases (Port in the OpenNMS socket task, and an ImageWriteMode alias planned for the dcm4che ImageWriteParam task), and today a reader sees only the alias name.

   Example (main @ cd49fea), the ImageWriteParam spec with

   @RefinementAlias("ImageWriteMode(int m) { m == ImageWriteParam.MODE_DISABLED || m == ImageWriteParam.MODE_DEFAULT || m == ImageWriteParam.MODE_EXPLICIT || m == ImageWriteParam.MODE_COPY_FROM_METADATA }")
   ...
   void setCompressionMode(@Refinement("ImageWriteMode(_)") int mode);

   and a client calling wParam.setCompressionMode(4):

   Refinement Error: mode == 4 is not a subtype of ImageWriteMode(mode)
   

   Besides the structured data for the IDE, the CLI message could keep the alias name and add its definition, once per alias used in Found or Expected:

   Refinement Error: mode == 4 is not a subtype of ImageWriteMode(mode)
     where ImageWriteMode(m) = m == ImageWriteParam.MODE_DISABLED || m == ImageWriteParam.MODE_DEFAULT
                               || m == ImageWriteParam.MODE_EXPLICIT || m == ImageWriteParam.MODE_COPY_FROM_METADATA
   
3. CatarinaGamboa

   added a commit that references this issue on Nov 5, 2026

   Keep a static final constant's name in refinement errors (#490)

   327a0d1
4. CatarinaGamboa

   closed this as completedin #489on Nov 5, 2026

Issue actions