Pith. sign in

REVIEW 4 major objections 6 minor 45 references

Guided Object-Oriented Development

T0 review · 4 major / 6 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2411.13200 v1 pith:7IUR2OJY submitted 2024-11-20 cs.SE

Harrie Passier , Lex Bijlsma , Ruurd Kuiper , Kees Huizing This is my paper · ORCID
classification cs.SE
keywords object-orienteddevelopmentproceduralguidancespecificationrefinementexternalandinternalspecificationssubspecificationsrobustnesssoftwaretestingprogrammingeducation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 6 minor

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.

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 (4)
  1. [Section 3, Robustness subsection] 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.
  2. [Section 3, Internal specification for removeAll] 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`.
  3. [Section 2.2, External Test] 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.
  4. [Section 6 and Section 4] 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.
minor comments (6)
  1. [Section 3, internal remove specification] The postcondition `@ensures mult(elem) = \old(mult(elem) - 1` is missing a closing parenthesis; it should be `\old(mult(elem)) - 1`.
  2. [Section 3, internal removeAll specification] The postcondition uses `\old(lst.size)` inconsistently; it should be `\old(lst.size())`, and the final conjunct should be written uniformly as `lst.size()`.
  3. [Section 2.2, External Test] The phrase 'All combinations coverage' should be 'all-combinations coverage' for consistency with the terminology used earlier in the same paragraph.
  4. [Section 2.2, External Test] 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.
  5. [Section 2.2, Code Test] 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.
  6. [Section 1 and Section 2.1] 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.

Circularity Check

0 steps flagged · score 1.0 of 10

No load-bearing circularity: the GOOD method's refinement obligations and organizational claims are not derived from their own conclusions, and the self-citations are background support rather than forced premises.

full rationale

The paper makes no quantitative prediction and contains no fitted parameter or equation whose output is reused as an input. The only formal-looking obligations are the three refinement rules in Section 2.2, stated as a definition of what it means for the internal specification to refine the external one ('the representation relation and internal postcondition should together imply the external postcondition'); those rules are not derived from the paper's conclusion that GOOD improves quality. The worked Bag example is illustrative, and Section 6 explicitly disclaims fundamental novelty: 'Examining the various activities involved in our approach reveals nothing fundamentally new; these activities, including all decisions needed, are already known in the literature... the novelty lies in organizing all the activities and decisions within a structured framework.' The paper does cite the authors' own technical report [41], tool paper [1], and earlier empirical work [4,5,8], but those citations supply background evidence (e.g., students' tests are incomplete, early test integration is beneficial) rather than a self-referential proof of the present claim; no uniqueness theorem or forced-choice argument is imported from them. The acknowledged limitation 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' is a boundary condition on the method, not a circular step. The robustness/removeAll inconsistencies in the example are correctness defects in the illustration, not cases where the example's conclusion is assumed to construct its own evidence. Accordingly the circularity score is 1: minor self-citations exist, but they are not load-bearing.

Assumptions & free parameters 0 free parameters · 3 assumptions · 2 invented entities

The approach depends not on numerical parameters but on pedagogical and specification-precision assumptions. The main postulated entities are the separately documented Internal View and the corresponding internal tests, both of which the authors claim as novelties. No free constants are fitted anywhere in the paper.

assumptions (3)
  • domain assumption Procedural guidance improves skill acquisition in complex tasks.
    Invoked from Merriënboer [33] in Section 1; the paper provides no direct evidence that this transfers to programming education.
  • domain assumption Informal natural-language specifications are precise enough to support refinement checks and test generation.
    Stated throughout Section 2 and discussed in Section 6 'Formality in specifications'; if precision is insufficient, the refinement rules cannot be verified.
  • domain assumption The three-view separation (external/internal/code) helps control complexity without losing consistency.
    Assumed throughout Section 2; the paper argues by example rather than by empirical evidence.
invented entities (2)
  • Internal View as a separate artifact (structure and behavior of private members)
    purpose: Provides implementers with a dedicated specification layer for private attributes and methods, distinct from client-facing specifications.
    The paper claims this view is new in Section 6; no outside falsifiable handle is provided beyond the framework itself.
  • Internal (grey-box) tests targeting a class's private internals
    purpose: Test private attributes, methods, and invariants that external black-box tests cannot reach.
    Claimed as new in Section 6; existing grey-box testing literature is cited, but the OO-class-specific application has no independent empirical validation.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Guided Object-Oriented Development." pith.science (2026). https://pith.science/paper/7IUR2OJY

@misc{pith2026241113200,
  author       = {Pith},
  title        = {Pith review of: Guided Object-Oriented Development},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7IUR2OJY}},
  note         = {Machine review of arXiv:2411.13200}
}
read the original abstract

To improve the quality of programs we provide an approach to guidance in the process of program development. At the higher level the various activities and their dependencies to structure the process are identified. At the lower level, detailed, practical rules are given for the decision-making in the development steps during these activities. The approach concentrates on structure and behavior of a single class. It includes design and specification and is compatible with methodologies for programming in the large. Informal specifications are introduced to help develop correct and robust code as well as corresponding tests. A strict distinction is made between external design and specification on one hand and internal design and specification on the other hand, which helps in keeping control over complexity. The approach also exploits the separation of success and failure scenarios. A worked-out example is provided.

Figures

Figures reproduced from arXiv: 2411.13200 by the authors.

Figure 1
Figure 1. Overview of the approach 6 [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. x is input for y x is input for y indicates that x produces insights and decisions that are input for an activity. An Analysis activity does not directly produce an artifact: it provides information to the activities that produce the artifacts. For the Bag example, one needs to analyse what a bag exactly is, and what external interface is desired [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. y needs x y needs x indicates that x needs information from y. This means that x and y may evolve together, and going back and forth between (working on) x and y is possible. It does also mean that on completing y, all information needed for x needs to be present, i.e., y can only be considered completed when x is completed - which requires checking this in the process. For the Bag example, for devising tests one ne… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: x results in y x results in y indicates that an activity results in an artifact. For the Bag example, this means that the specifications, annotated code and tests are avail￾able. The procedural guidance is flexible with respect to the order of steps and their repetitio…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

45 extracted references · 44 canonical work pages

  1. [1]

    Towards a tool to support students through procedural program- ming guidance

    Sander Albers, Nando Reij, Wouter Brinksma, Lex Bijlsma, and Harrie Passier. Towards a tool to support students through procedural program- ming guidance. In Proceedings of the 11th Computer Science Education Research Conference, pages 13–23, 2022

    work page 2022

  2. [2]

    Test-driven development: by example

    Kent Beck. Test-driven development: by example . Addison-Wesley Profes- sional, 2003

    work page 2003

  3. [3]

    A. Bijlsma. Model-based specification. Information Processing Letters , 77(2):77–84, 2001

    work page 2001

  4. [4]

    Bijlsma, N

    A. Bijlsma, N. Doorn, H. Passier, H. Pootjes, and S. Stuurman. How do students test software units? In IEEE/ACM 43rd International Conference on Software Engineering: Software Engineering Education and Training (ICSE-SEET 2021) , pages 189–198, 2021

    work page 2021

  5. [5]

    Bijlsma, H.J.M

    A. Bijlsma, H.J.M. Passier, H.J. Pootjes, and S. Stuurman. Integrated test development: An integrated and incremental approach to write software of high quality. In 7th Computer Science Education Research Conference (CSERC 2018, pages 9–20, 2018

    work page 2018

  6. [6]

    Robert V. Binder. Testing object-oriented systems: models, patterns, and tools. Addison-Wesley Longman Publishing Co., Inc., USA, 1999

    work page 1999

  7. [7]

    The unified modeling language user guide

    Grady Booch, James Rumbaugh, and Ivar Jacobson. The unified modeling language user guide . Addison-Wesley, Upper Saddle River, NJ, 2005

    work page 2005

  8. [8]

    Improving students' code correctness and test completeness by informal specifications

    Arno Broeders, Ruud Hermans, Sylvia Stuurman, Lex Bijlsma, and Harrie Passier. Improving students’ code correctness and test completeness by informal specifications. arXiv preprint arXiv:2309.02221 , 2023

    work page Pith review arXiv 2023

Show all 45 references
  1. [9]

    Yoonsik Cheon and Gary T. Leavens. A simple and practical approach to unit testing: The JML and JUnit way. In European Conference on Object-Oriented Programming, pages 231–255. Springer, 2002

    2002

  2. [10]

    Systematic testing should not be a topic in the com- puter science curriculum! ACM Sigcse Bulletin , pages 7–10, 09 2003

    Henrik Christensen. Systematic testing should not be a topic in the com- puter science curriculum! ACM Sigcse Bulletin , pages 7–10, 09 2003

    2003

  3. [11]

    A Discipline of Programming

    Edsger Wybe Dijkstra. A Discipline of Programming . Prentice-Hall, 1976

    1976

  4. [12]

    Edsger Wybe Dijkstra and Wim H.J. Feijen. A Method of Programming . Addison-Wesley, 1988

    1988

  5. [13]

    Lydie Du Bousquet, Yves Ledru, Olivier Maury, Catherine Oriat, and J.- L. Lanet. A case study in JML-based software validation. In Proceedings. 19th International Conference on Automated Software Engineering, 2004. , pages 294–297. IEEE, 2004. 33

    2004

  6. [14]

    Edwards and Z

    S. Edwards and Z. Shams. Do student programmers all tend to write the same software tests? In IT in Computer Science Education (ITiCSE 2014), pages 171–176, 2014

    2014

  7. [15]

    How to Design Programs

    Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi. How to Design Programs. An Introduction to Computing and Programming. The MIT Press, Cambridge, Massachusetts London, England, 2001. MIT – Massachusetts Institute of Technology – Online ver- si...

    2001

  8. [16]

    Gegg-Harrison, Gary R

    Timothy S. Gegg-Harrison, Gary R. Bunce, Rebecca D. Ganetzky, Christina M. Olson, and Joshua D. Wilson. Studying program correctness by constructing contracts. In Proceedings of the 8th annual conference on Innovation and technology in computer science education , pages 129–133, 2003

    2003

  9. [17]

    Ghezzi, M

    C. Ghezzi, M. Jazayeri, and D. Mandrioli. Fundamentals of Software En- gineering. Prentice Hall PTR, 2002

    2002

  10. [18]

    The Science of Programming

    David Gries. The Science of Programming . Springer, 1981

    1981

  11. [19]

    Java unit testing with JUnit 5

    Shekhar Gulati and Rahul Sharma. Java unit testing with JUnit 5. In Java Unit Testing with JUnit . Springer, 2017

    2017

  12. [20]

    C. A. R. Hoare. Proof of correctness of data representations. Acta infor- matica, 1(4):271–281, 1972

    1972

  13. [21]

    Software testing: a craftsman ’s approach

    Paul C Jorgensen. Software testing: a craftsman ’s approach . Auerbach Publications, 2013

    2013

  14. [22]

    Kruchten

    P. Kruchten. The Rational Unified Process: an Introduction . Addison- Wesley Professional, 2004

    2004

  15. [23]

    C. Larman. Applying UML and Patterns: An Introduction to Object- Oriented Analysis and Design and Iterative Development (3rd Edition) . Prentice Hall PTR, 2004

    2004

  16. [24]

    Leavens and C

    G.T. Leavens and C. Baker, A.L. Ruby. JML: A notation for detailed design. In Behavioral specifications of Businesses and Systems , pages 175–

  17. [25]

    Rustan M

    K. Rustan M. Leino. Constructing a program with exceptions. Information processing letters, 53(3):159–163, 1995

    1995

  18. [26]

    Program Proofs

    K Rustan M Leino. Program Proofs. MIT Press, 2023

    2023

  19. [27]

    Rustan M

    K. Rustan M. Leino and Greg Nelson. Data abstraction and informa- tion hiding. ACM Transactions on Programming Languages and Systems (TOPLAS), 24(5):491–553, 2002. 34

    2002

  20. [28]

    Rustan M

    K. Rustan M. Leino and Valentin W¨ ustholz. The Dafny integrated devel- opment environment. arXiv preprint arXiv:1404.6602, 2014

    2014 arXiv

  21. [29]

    Program Development in Java: Abstrac- tion, Specification, and Object-Oriented Design

    Barbara Liskov and John Guttag. Program Development in Java: Abstrac- tion, Specification, and Object-Oriented Design. Addison-Wesley Longman Publishing Co., Inc., USA, 1st edition, 2000

    2000

  22. [30]

    Ab- straction mechanisms in clu

    Barbara Liskov, Alan Snyder, Russell Atkinson, and Craig Schaffert. Ab- straction mechanisms in clu. Commun. ACM, 20(8):564–576, aug 1977

    1977

  23. [31]

    Liskov and Jeannette M

    Barbara H. Liskov and Jeannette M. Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems (TOPLAS), 16:1811–1841, 1994

    1994

  24. [32]

    Integrating specification-based review and testing for detect- ing errors in programs

    Shaoying Liu. Integrating specification-based review and testing for detect- ing errors in programs. In International Conference on Formal Engineering Methods, pages 136–150. Springer, 2007

    2007

  25. [33]

    Merri¨ enboer and Paul A

    Jeroen G. Merri¨ enboer and Paul A. Kirschner.Ten Steps to Complex Learn- ing. Routledge, 2007

    2007

  26. [34]

    Object-Oriented Software Construction

    Bertrand Meyer. Object-Oriented Software Construction . Prentice-Hall, 2nd edition, 1997

    1997

  27. [35]

    Design by Contract

    Bertrand Meyer. Design by Contract . Prentice-Hall, 2002

    2002

  28. [36]

    Programming from Specifications

    Carroll Morgan. Programming from Specifications. Prentice-Hall, 1990

    1990

  29. [37]

    J.M. Morris. Laws of data refinement. Acta Informatica, 26:287–308, 1989

    1989

  30. [38]

    Paige and Jonathan S

    Richard F. Paige and Jonathan S. Ostroff. Specification-driven design with Eiffel and agents for teaching lightweight formal methods. In International Conference on Technical Formal Methods, pages 107–123. Springer, 2004

    2004

  31. [39]

    Precise documentation: The key to better software

    David Lorge Parnas. Precise documentation: The key to better software. In The Future of Software Engineering , pages 125–148. Springer, 2011

    2011

  32. [40]

    D.L. Parnas. On the criteria to be used in decomposing systems into mod- ules. Communications of the ACM , 15:1053–1058, 1972

    1972

  33. [41]

    Specification based OO-development: Procedural guidance

    Harrie Passier, Lex Bijlsma, and Ruurd Kuiper. Specification based OO-development: Procedural guidance. Technical Report OUNL-CS-2022-6, Open universiteit, Heerlen, The Netherlands, 2022. Online at https://research.ou.nl/en/publications/specification-based-oo- development-proc...

    2022

  34. [42]

    Exploring stu- dents’ understanding of the concept of algorithm: levels of abstraction

    Jacob Perrenet, Jan Friso Groote, and Eric Kaasenbrood. Exploring stu- dents’ understanding of the concept of algorithm: levels of abstraction. ACM SIGCSE Bulletin , 37(3):64–68, 2005. 35

    2005

  35. [43]

    Teaching cps foundations with contracts

    Andr´ e Platzer. Teaching cps foundations with contracts. Carnegie Mellon University, 2013

    2013

  36. [44]

    Furia, Yu Pei, Yi Wei, and Bertrand Meyer

    Nadia Polikarpova, Carlo A. Furia, Yu Pei, Yi Wei, and Bertrand Meyer. What good are strong specifications? In 2013 35th International Confer- ence on Software Engineering (ICSE) , pages 262–271. IEEE, 2013

    2013

  37. [45]

    N. Wirth. Program development by stepwise refinement. Communications of the ACM , 14:221–227, 1971. 36

    1971

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.