Protocol: how the pool of sources was built

This file records how the algorithm-design review was searched, screened and scored, for a reviewer who wants to repeat it. The rules every review shares are in the evidence method. Every search of this review ran on 2026-10-29. Two neighbouring reviews cover the rest: pseudocode and flowcharts are in pseudocode and decision records are in design decisions.

1. Why grey literature

Garousi 2019 Table 4 asks seven questions, and one yes is enough to add grey literature (the rule). Here all seven are yes.

# Question Answer for this topic
1 Complex, not solvable from formal literature alone? yes: specification styles come from languages and tools
2 Lack of volume or quality of evidence? yes: 17 controlled trials among 94 papers on teaching algorithm design (Liu 2024b)
3 Context important? yes: safety-critical work and a web service ask different things of a specification
4 Corroborate research with practice? yes
5 Challenge practice with research, or the reverse? yes: spec-driven tools run ahead of any effect study (position.md)
6 Would a synthesis serve both communities? yes
7 Large practitioner volume? yes: 143,670 stars on one spec-driven tool; 9,114 on a property-testing library (sources.md)

2. Questions

Id Question
Q1 Which design techniques are taught and used, and is their taxonomy sound?
Q2 Does problem solving instruction improve the algorithms people produce?
Q3 Which ways of stating intended behaviour exist?
Q4 Do specifications improve correctness, and at what cost?
Q5 Are formal notations readable?
Q6 What does practice use?
Q7 How are algorithms engineered and evaluated by experiment?
Q8 Does a specification or a plan given to a model improve its code?

3. Existing reviews (Garousi Guideline 2)

  • Searched first, by eight web searches (R1 to R8) on the first result page, about ten results each.
    • R1 teaching algorithm design techniques, systematic review.
    • R2 formal specification, mapping study, empirical evidence, cost.
    • R3 language models for code generation, planning and specification, survey.
    • R4 design by contract and run-time assertion checking, systematic review.
    • R5 property-based testing, mapping study or review (two result lists).
    • R6 formal methods education, systematic review.
    • R7 programming problem solving and planning for novices, systematic review (two result lists).
    • R8 language models and formal specification, survey.
  • Found: 9 reviews, maps and surveys; 1 read in part (Liu 2024b), 2 by abstract (Okumus 2025, Beg 2025), the rest by abstract summary or title. They are in review.md strand 0.
  • R5 found no review of property-based testing; R7 found no review of planning strategies on novice outcomes.

6. Stopping rule

  • Fixed before searching: effort bounded at N = 10 results per string, with saturation at k = 5. Five consecutive results that add no new concept end a string; G2 and G3 ended this way, since the next results repeated known sources.
  • Formal: effort bounded (top 10 per string), plus evidence exhaustion for the small sets (F3, F15, F16, F18, under 50).
  • Q/A sites: the parameters are in the subsection above.

7. Selection

  • Include: a source on designing an algorithm, on stating what it must do, on the evidence of effect or cost, or on handing either to a model; English; readable on the search date.
  • Exclude:
    • verification tools and test generators with no bearing on the question (adjacent only);
    • sources on pseudocode, flowcharts, diagrams, decision records and distributed-system design, which other topics own;
    • vendor posts selling a product with no practice content;
    • sources whose abstract could not be read and whose title does not settle relevance.
  • Grey sources must also pass section 8.

8. Quality of grey sources (Garousi Guideline 11, Table 7)

  • The 20 criteria, the tier scale and the threshold of 10 of 20 are those of the evidence method.
  • Tiers as applied here: tier 1 is books, magazines, theses, standards and committee documents and vendor guidance pages. Tier 2 is presentations, project documentation, repository pages and wiki and Q/A pages. Tier 3 is blogs.
  • Impact is judged from stars, downloads, citations, views or votes, as the source allows.
  • A source below the threshold stays only an example of practice, never support for a claim.
  • Scores, with subtotals, are in sources.md.

9. Extraction and synthesis

  • Extraction and synthesis follow the evidence method; the synthesis runs by question, Q1 to Q8.
  • A grey source never raises a claim above convention; it shows adoption, with the number, its source and its date.

10. Limits

  • The limits shared by every review are in the evidence method.
  • One reviewer, no second rater, no inter-rater agreement.
  • The Semantic Scholar lists are ordered by citations. Forward snowballing was not run; backward covered one review.
  • Sources read by title only support no claim.
  • Sobel 2002 was not read as a paper, only through its published comment; Levitin 1999 was read in full later, through a library.
  • The main books (Polya, Gries, Kourie, Abrial, Back, McGeoch, Kleinberg, Skiena) were not opened.
  • Benchmarks of models age within months; the numbers in strand 7 are those of the abstracts.
  • This search did not find a controlled study of specification against none on algorithms people write, nor a test of a taxonomy of design techniques; that is not proof none exists.
  • Q/A threads: one scorer, no second rater.