{"id":"79c0a859-3cb5-4085-bba9-ac90ba39d99f","arxiv_id":"2411.13200","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":4.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"GOOD organizes object-oriented class development around external, internal, and code views, adds separate internal tests, and structures robustness via subspecifications.","lead":"This paper proposes GOOD, a step-by-step guidance framework for developing one object-oriented class at a time, with separate external, internal, and code views and tests for each view. A worked Bag example illustrates the process, but the paper offers no empirical evidence that the approach improves code quality or test completeness.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The worked example fails the method's own check: the robustness subspecification for remove is never reflected in the implementation shown, and the removeAll internal postcondition is contradictory as written; without a corrected reproducible example and an evaluation, the 'more comprehensive…","rationale":"The reader's conditional verdict is sound: the paper is clear, honest about novelty, and the main gap is the absence of a controlled evaluation. I partly agree, but the sharpest weak point is not only missing empirical evidence; it is that the paper's own worked example is internally inconsistent at the exact point the method is supposed to add value - robustness. The Robustness section specifies an exception behavior but does not update the implementation, and the removeAll internal specification is contradictory as written. This makes it impossible to verify the claimed link from subspecifications to tests and casts doubt on whether the three-view refinement obligations are actually enforced in practice. A typo in a worked example would normally be minor, but here it occurs in the central demonstration of the method's distinctive mechanism. Because the concern can be addressed by a corrected example and by an evaluation (or by reframing the paper as a didactic proposal without a demonstrated improvement claim), conditional acceptance remains the right verdict; rejection would be too strong given the honest framing and the plausible didactic value of the guidance.","tokens_in":17125,"tokens_out":7532,"duration_ms":79326,"concrete_test":"Reproduce Section 3 as a runnable JUnit project: implement the Bag with the robust remove branch (throw ArgumentNotFoundException when elem is absent), correct the removeAll postcondition to `mult(elem)==0`, generate tests exactly by the paper's three-step guidance (equivalent classes/boundaries, all-combinations coverage), and compute the mutation score against a small mutant set (wrong exception type for remove(10), removeAll leaves one duplicate, size off by one, remove removes wrong occurrence). If the GOOD-derived suite does not kill these mutants, the high-coverage claim and the quality-improvement claim fail; if it does, the concern reduces to a presentation defect.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim depends on the chain: informal specifications -> refinement obligations -> tests -> better code. Section 2 (Internal Specification) makes refinement checkable via three implication rules, and External Test promises high coverage via a three-step translation. Two things break this chain. First, Section 6 concedes that without tool feedback 'the quality of the formal specifications that the students produce is often too low' - in the very educational setting the method targets. Second, and more concretely, Section 3's own artifacts violate the workflow. The Robustness subsection adds external/internal subspecifications for remove with @signals ArgumentNotFoundException for the absent-element case, but the Annotated Code shown earlier still has the non-robust body (int here = lst.indexOf(elem); lst.remove(here);), which for b1.remove(10) would raise IndexOutOfBoundsException, not ArgumentNotFoundException. The following test expects the specified exception, so the example does not demonstrate what it claims. The internal postcondition for removeAll is also written as `@ensures ! mult(elem) = 0`, which is either syntactically invalid or, read as `mult(elem) != 0`, contradicts the external postcondition `B(elem)=0`. These are not mere typos: the method's core premise is that each subspecification is separately implemented and tested, and its showcase fails that check.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper introduces Guided Object-Oriented Development (GOOD), a procedural framework for developing a single Java class with explicit external, internal, and code views. The approach combines JML-like informal specifications, a strict external/internal distinction, subspecifications for happy and non-happy paths, and a structured derivation of black-box, grey-box, and white-box tests. The paper presents the framework, a worked Bag example, a brief tool description, a related-work survey, and conclusions. The central claim is that following this guidance leads to better-structured specifications, more readable code, and more comprehensive testing.","tokens_in":17368,"tokens_out":5265,"duration_ms":53214,"significance":"The explicit separation of external and internal specifications with three refinement obligations, the use of subspecifications for robustness, and the systematic translation of views into tests are useful pedagogical ideas. The authors are transparent that the full method is elaborated in a technical report and that no empirical validation is included. However, the central claim of improved quality and test completeness is not supported by evidence, and the only worked example contains internal inconsistencies that violate the method's own refinement rules. If the example and the unsupported coverage claims are corrected, the framework could be a useful contribution to software-engineering education, but in its current form the paper does not demonstrate the benefits it advertises.","major_comments":[{"comment":"The external and internal subspecifications for remove specify `@signals ArgumentNotFoundException(\"Elem is not present\")` for the case `B(elem)=0`, and the test section expects `b1.remove(10)` to produce this exception. However, the Annotated Code View shown earlier in the same section implements remove as `int here = lst.indexOf(elem); lst.remove(here);`, so `b1.remove(10)` with `b1={2,2,6,4}` calls `lst.remove(-1)`, which raises `IndexOutOfBoundsException` rather than `ArgumentNotFoundException`. This is not a mere typographical slip: the example does not demonstrate the method's central claim that each subspecification is separately implemented and tested.","section":"Section 3, Robustness subsection"},{"comment":"The internal postcondition for `removeAll` is written as `@ensures ! mult(elem) = 0`. As written, this is either syntactically invalid or, reading `!` as negation, asserts `mult(elem) != 0`, which contradicts the external postcondition `@ensures B(elem) = 0` and the intended semantics of removing all instances. Because Section 2.2 requires the internal postcondition to imply the external postcondition, this single postcondition violates the method's own refinement rule. It should read `@ensures mult(elem) = 0`.","section":"Section 3, Internal specification for removeAll"},{"comment":"The text states that translating the External View stepwise into tests 'results in a test with a high test coverage' without defining what coverage means or providing any measurement. Given that the abstract and introduction claim improved code quality and more comprehensive testing, this unsupported assertion is load-bearing. The paper should either present empirical evidence of the coverage achieved by the three-step translation or explicitly rephrase the claim as a hypothesis.","section":"Section 2.2, External Test"},{"comment":"The authors concede in Section 6 that 'without tools that interpret the specifications and provide feedback, the quality of the formal specifications that the students produce is often too low to reap these benefits.' The tool described in Section 4 is said to 'aim to guide' students, but no evaluation of the tool is provided. Since the intended users are students and the central claim concerns improving their programs and tests, the paper should either present data showing the approach works in the intended educational setting or explicitly re-scope the contribution as an untested proposal requiring tool support.","section":"Section 6 and Section 4"}],"minor_comments":[{"comment":"The postcondition `@ensures mult(elem) = \\old(mult(elem) - 1` is missing a closing parenthesis; it should be `\\old(mult(elem)) - 1`.","section":"Section 3, internal remove specification"},{"comment":"The postcondition uses `\\old(lst.size)` inconsistently; it should be `\\old(lst.size())`, and the final conjunct should be written uniformly as `lst.size()`.","section":"Section 3, internal removeAll specification"},{"comment":"The phrase 'All combinations coverage' should be 'all-combinations coverage' for consistency with the terminology used earlier in the same paragraph.","section":"Section 2.2, External Test"},{"comment":"The sentence contrasting test derivation with TDD ('instead of a test functioning as (partial) specification, as in tdd [2]') is awkardly phrased and should be rewritten to state clearly that GOOD derives tests from explicit specifications, whereas TDD treats tests as an executable specification.","section":"Section 2.2, External Test"},{"comment":"The phrase 'we consider code testing as foreknowledge' is unclear; it likely means that code testing is considered prerequisite knowledge, but the wording should be made explicit.","section":"Section 2.2, Code Test"},{"comment":"The paper claims that the approach leads to 'well-structured specifications' but does not define what 'well-structured' means; a precise criterion or at least a list of properties would make the claim falsifiable.","section":"Section 1 and Section 2.1"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is more of a teaching-methods position paper than an empirical software-engineering study. If the venue expects empirical validation for claims about improved code quality and test completeness, the paper would need a substantial evaluation component. At minimum, the worked example must be corrected so that the robustness subspecification is implemented and the internal postconditions satisfy the refinement rules stated in Section 2.2. The authors are honest that the full method is in a technical report, but the paper as submitted is not self-contained enough to support its central claims."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Nothing fundamentally new here, and the authors say so themselves: the individual activities come from Liskov-Guttag, Leino-Nelson, and the refinement tradition. What the paper adds is an organized framework—three views (external, internal, code), internal tests as a first-class artifact, and robustness handled through subspecifications. That organization can be genuinely useful for teaching, and the writing is refreshingly candid about where the novelty sits. The related-work section is fair, and the worked Bag example helps make the guidance concrete.\n\nBut the central claim that the approach \"leads to ... more comprehensive testing\" and \"improve[s] the quality of programs\" is asserted, not demonstrated. The external-test section claims the three-step translation \"results in a test with a high test coverage\" with no measurement attached. And the worked example fails the method's own check. In the Robustness subsection, the authors add external and internal subspecifications for remove that require ArgumentNotFoundException when the element is absent, yet the annotated code shown earlier still has the plain body `lst.remove(lst.indexOf(elem))`, which for an absent element would throw IndexOutOfBoundsException, not the specified exception. The test later expects the specified exception, so the artifact is out of sync with the spec. Also, the removeAll internal postcondition `@ensures ! mult(elem) = 0` contradicts the external postcondition `B(elem)=0` (unless it is meant to be `mult(elem) = 0`). Because the method's whole premise is that subspecifications are implemented separately and tested, these are not cosmetic typos. A reader who follows the example closely will see the approach's own discipline violated in the showcase.\n\nThere is also a deeper uncertainty the paper admits in Section 6: without tools that check the specs, student-produced specifications are \"often too low\" in quality. That admission sits in tension with the claim that the approach, as presented, will help typical students.\n\nOn balance, this is a serious, readable methods paper with a real gap between the framework's promise and the evidence behind it. I'd send it to review at a SE-education venue, but the referee should insist on a corrected example and either a small empirical evaluation (even a classroom study) or a reframing as a didactic proposal without an improvement claim. The framework itself may well help; the paper as written overreaches.","headline":"A candid, well-organized teaching framework whose central improvement claim is unmeasured and whose Bag example violates the method's own refinement rules; revise before acceptance.","tokens_in":17910,"tokens_out":2712,"would_cite":false,"duration_ms":27057,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper argues that a three-view class-development structure—external, internal, and code—with refinement rules and failure subspecifications yields more readable code and more complete tests.","keywords":["object-oriented development","procedural guidance","specification refinement","external and internal specifications","subspecifications","robustness","software testing","programming education"],"falsifier":"Run a controlled classroom study in which students build the same class with GOOD guidance and with their usual process, then score the resulting test suites by statement and branch coverage and by how many seeded defects they detect; if the GOOD group is not clearly better on either measure, the paper's central quality claim fails.","tokens_in":16905,"feed_emoji":"🧭","tokens_out":7781,"duration_ms":75600,"temperature":0.7,"pith_summary":"The paper proposes Guided Object-Oriented Development (GOOD), a method for developing a single class that tells students and programmers what development steps to take and how to make the decisions at each step. Its central proposal is to keep three views of the class—external (the API and public behavior), internal (private attributes and refined specifications), and code (the annotated implementation)—and to derive a matching test type from each view. Correctness is carried from the public specification to the implementation by a representation relation and class invariants, with refinement rules the internal view must satisfy. Failure behavior is treated explicitly as subspecifications, so robustness is designed and tested rather than added at the end. The intended payoff is that code becomes more readable and tests become more complete, catching defects earlier in programming education and in real development.","feed_headline":"Three views carry a class from specification to tested code","feed_subtitle":"Each view produces its own tests, so testing starts as soon as the specification exists.","key_machinery":"The load-bearing object is the three-view artifact and the representation relation that connects views. Each class has an External View (public signatures plus @inv, @requires, @ensures), an Internal View (private attributes and methods, refined specifications, and a @represents clause), and an Annotated Code View (implementation with comments and specs). The representation relation and internal invariants do the correctness work: the paper states three refinement rules—that the representation relation with the internal invariant implies the external invariant, that it carries external preconditions into internal preconditions, and that internal postconditions discharge external postconditions. Subspecifications are the second mechanism: they split a method's contract into separate cases, notably the happy path and failure paths, each generating its own tests and informing the control-flow structure of the body.","core_discovery":"The central claim is that dividing a class into three views, refining the public specification into an internal one, and specifying failure behavior separately yields specifications that support readable code and fuller tests. The mechanism is the strict separation of an External View for clients from an Internal View for implementers, where the internal specification is a refinement of the external one; a @represents clause explains how domain concepts map to class attributes, and three proof obligations tie the two specifications together. Each view produces its own tests—blackbox from the external spec, greybox from the internal spec, and whitebox from the code—so testing is integrated throughout development instead of being postponed. Robustness is handled by splitting specifications into subspecifications for happy and unhappy paths, with @signals describing exceptions; the worked Bag example shows the same subspecifications structuring the implementation and the tests. The authors conclude that the novelty is organizational: no single activity is new, but arranging known activities into these views and giving procedural rules for each decision point is.","pith_inferences":["Editorial inference: the refinement rules are machine-checkable; plugging a contract verifier into GOOD could compensate for the unreliable informal specifications the authors flag as a weakness.","Editorial inference: the three-view structure transfers to other languages with pre/postcondition support, since the method hinges on the representation relation, not on Java or JML syntax.","Editorial inference: a natural empirical test is a controlled course experiment measuring test coverage and seeded-defect detection for students using GOOD versus a standard procedure; the paper does not report such data.","Editorial inference: the separation of failure subspecifications predicts that students will write more exception-path tests than with happy-path-only development; that prediction can be checked by inspecting test suites."],"forward_implications":["External (blackbox) tests can be written as soon as the external specification exists, so test-first advantages appear without committing to a rigid test-first order.","Internal (greybox) tests reach private attributes and methods, exposing defects blackbox testing cannot see and giving extra boundary cases from class invariants.","Subspecifications for failure inputs make exception behavior an explicit part of design and testing, with each failure case getting its own test.","The three refinement rules give students a concrete way to check that the internal view faithfully implements the external view, so correctness can be argued before coding finishes.","Because the activities are interrelated rather than sequential, the same process accommodates different ordering strategies, from design-pattern-first to data-refinement-first."],"supporting_citations":[{"why":"supplies the theory of procedural knowledge that motivates stepwise guidance for complex tasks.","marker":"[33]"},{"why":"grounds the external/internal specification split and the information-hiding principle the internal view respects.","marker":"[27]"},{"why":"provides the class/method design-and-specification style that GOOD organizes into views.","marker":"[29]"},{"why":"gives data-refinement laws used for the relation between external and internal specifications.","marker":"[37]"},{"why":"contributes stepwise refinement as the basis for internal specifications refining external ones.","marker":"[45]"},{"why":"supplies the JML-style tags (@requires, @ensures, @inv) used in all views.","marker":"[24]"},{"why":"supports writing tests early and incrementally, which GOOD builds into the activities.","marker":"[5]"},{"why":"shows failure behavior can be specified like success behavior, the basis for robustness subspecifications.","marker":"[25]"},{"why":"describes the tool that projects the three views from one master artifact and keeps them in sync.","marker":"[1]"},{"why":"contains the full elaboration of the activities and rules summarized in this paper.","marker":"[41]"}],"fun_headline_variants":["Three views guide a class from spec to tested code","External and internal views each produce their own tests","Separate external from internal specs to get robust, tested code","Specify failure paths to build robust code and tests","Blackbox, greybox, whitebox: three test layers from one class spec"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that informal, natural-language specifications can be precise enough for students to check the internal refinement rules and to turn each subspecification into meaningful tests; if the specifications are vague, the guidance gives no reliable check and the tests lose their power.","fun_headline_variants_meta":{"raw":{"variants":["Three views guide a class from spec to tested code","External and internal views each produce their own tests","Separate external from internal specs to get robust, tested code","Specify failure paths to build robust code and tests","Blackbox, greybox, whitebox: three test layers from one class spec"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001158,"raw_usage":{"total_tokens":4753,"prompt_tokens":856,"completion_tokens":3897,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":472,"completion_tokens_details":{"reasoning_tokens":3814}},"tokens_in":472,"tokens_out":3897,"duration_ms":27919,"temperature":1.0,"reasoning_tokens":3814,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T16:42:09.630236+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run a controlled classroom study in which students build the same class with GOOD guidance and with their usual process, then score the resulting test suites by statement and branch coverage and by how many seeded defects they detect; if the GOOD group is not clearly better on either measure, the paper's central quality claim fails.","supporting_citations":[{"cited_title":"Merri¨ enboer and Paul A","cited_arxiv_id":null,"evidence_quote":"supplies the theory of procedural knowledge that motivates stepwise guidance for complex tasks."},{"cited_title":"Rustan M","cited_arxiv_id":null,"evidence_quote":"grounds the external/internal specification split and the information-hiding principle the internal view respects."},{"cited_title":"Program Development in Java: Abstrac- tion, Specification, and Object-Oriented Design","cited_arxiv_id":null,"evidence_quote":"provides the class/method design-and-specification style that GOOD organizes into views."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"gives data-refinement laws used for the relation between external and internal specifications."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"contributes stepwise refinement as the basis for internal specifications refining external ones."},{"cited_title":"Leavens and C","cited_arxiv_id":null,"evidence_quote":"supplies the JML-style tags (@requires, @ensures, @inv) used in all views."},{"cited_title":"Bijlsma, H.J.M","cited_arxiv_id":null,"evidence_quote":"supports writing tests early and incrementally, which GOOD builds into the activities."},{"cited_title":"Rustan M","cited_arxiv_id":null,"evidence_quote":"shows failure behavior can be specified like success behavior, the basis for robustness subspecifications."},{"cited_title":"Towards a tool to support students through procedural program- ming guidance","cited_arxiv_id":null,"evidence_quote":"describes the tool that projects the three views from one master artifact and keeps them in sync."},{"cited_title":"Specification based OO-development: Procedural guidance","cited_arxiv_id":null,"evidence_quote":"contains the full elaboration of the activities and rules summarized in this paper."}],"review_version":1}