Skip to content

Warn when a state set is named like a method of its class #514

Closed

Description

@CatarinaGamboa

Problem

With named state sets (#498), a set whose name is also the name of a method makes every state error look like a call to that method. In the undo manager spec the sets are named undo and redo. Real output on main (0.0.37):

State Refinement Error: expected undo(undoManager) == undoable but could not prove it
21 |         undoManager.undo();
   |         ^^^^^^^^^^^^^^^^^^^

A Java developer reads undo(undoManager) as "the result of undoManager.undo()", which is the very call that failed. A UX review and a verification review of the named-set messages both ranked this as the highest risk for the error-message study: it is a confound that has nothing to do with the messages themselves.

Proposal

  1. Warning (not an error, nothing is ambiguous for the verifier) when a @StateSet name equals the name of a method of the class it is declared on. For @ExternalRefinementsFor specs, check the methods declared in the spec interface, which are the target's refined methods. Suggested text:
    State set name 'undo' is also the name of a method of UndoManager, so undo(x) == undoable reads like a call to undo(). Choose another name, such as undoState
  2. Rename the sets in the fixtures that use clashing names. For example, state_hint_study_undo_manager_correct/UndoManagerRefinementsExpert.java uses phase/undo/redo; rename them to phase/undoState/redoState.
  3. Docs (Document named state sets and states written as values of their sets #512 added named sets to the docs): one sentence advising set names that do not clash with method names.

When the study specs get set names, they must not clash. Today they use none.

Tests

Extend ErrorStateSetNames (or the closest existing fixture) with one clashing set: // Expect: Warning. No new fixture class unless needed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    studyNeeded before the error-message user study

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions