Programming Logic Foundations: Thinking Like a Programmer

New course

10 pages

All courses > Information Technology > Programming logic ::

Capstone Logic Workshop: From Specification to a Verified Procedure

Capítulo 10

Estimated reading time: 7 minutes

+ Exercise

This workshop is an end-to-end, staged deliverable that takes one problem from an initial specification to a procedure you can justify as correct. The emphasis is on producing artifacts you could hand to someone else: a spec document, an algorithm representation, trace logs, and a correctness checklist.

Workshop Problem

Problem statement (informal): Given a list of time intervals during a day, compute the total number of minutes covered by at least one interval (overlaps should not be double-counted).

Example: intervals [09:00–10:00, 09:30–11:00] cover 120 minutes total (09:00–11:00), not 150.

Deliverable 1: Specification Document

1) Goal (clarified)

Compute the total covered duration (in minutes) of the union of intervals. Intervals may overlap or touch. The result counts each minute at most once.

2) Inputs and outputs

Input: A list of intervals. Each interval has a start and end time within the same day.
Representation: Convert times to integer minutes since midnight (0..1440). Each interval is a pair (startMin, endMin).
Output: An integer totalCoveredMinutes.

3) Constraints and interpretation decisions

Topic	Decision	Why it matters
Interval boundaries	Use half-open intervals: `[start, end)`	Prevents double-counting when intervals touch (e.g., [60,120) and [120,180) share no minutes).
Validity	Each interval must satisfy `0 ≤ start ≤ end ≤ 1440`	Ensures a well-defined duration and day bounds.
Empty intervals	Allow `start == end` (duration 0)	Should not affect the total.
Ordering	Intervals may be unsorted	Algorithm must not assume input order.
Duplicates	Duplicates may exist	Should not change the union length.

4) Subproblems (decomposition as deliverables)

Normalize: Ensure all intervals are in minutes and valid.
Order: Sort intervals by start time (and by end time as a tie-breaker).
Merge/accumulate: Walk through sorted intervals, merging overlaps/touches and accumulating covered minutes.
Return: Output the accumulated total.

5) Acceptance criteria (what must be true)

Overlapping intervals are not double-counted.
Touching intervals (end == next start) are treated as continuous coverage under half-open semantics (no gap, no overlap).
Result is deterministic: same input list yields the same integer output.
Works for empty input (returns 0) and for single interval.

Deliverable 2: Algorithm Representation (Language-Agnostic Pseudocode)

Pseudocode

PROCEDURE TotalCoveredMinutes(intervals):  # intervals are pairs (start, end) in minutes, [start, end) semantics    IF intervals is empty:        RETURN 0    # Step 1: sort by start ascending, then end ascending    sorted = intervals sorted by (start, end)    total = 0    currentStart = sorted[0].start    currentEnd   = sorted[0].end    FOR each interval (s, e) in sorted starting from index 1:        IF s > currentEnd:            # gap: finalize current merged interval            total = total + (currentEnd - currentStart)            currentStart = s            currentEnd = e        ELSE:            # overlap or touch: extend if needed            currentEnd = MAX(currentEnd, e)    # finalize last merged interval    total = total + (currentEnd - currentStart)    RETURN total

Notes that tighten the procedure

Half-open intervals: The condition s > currentEnd detects a true gap. If s == currentEnd, the intervals touch and are merged, which is consistent with union length under [start,end) (no double-counting).
Tie-breaker in sorting: Sorting by end when starts are equal makes the merge step simpler to reason about (the first interval among equal starts has the smallest end, but the MAX update handles all cases).

Deliverable 3: Trace Logs (Test-Driven Tracing)

Trace logs are written as if you are “executing by hand,” recording state changes. The goal is to confirm the algorithm’s behavior on representative cases and to expose ambiguous spec decisions early.

Continue in our app.

You can listen to the audiobook with the screen off, receive a free certificate for this course, and also have access to 5,000 other free online courses.

Or continue reading below...

Download the app

Trace Log Format

sorted: the ordered intervals
(currentStart, currentEnd): current merged interval
total: accumulated covered minutes so far
decision: gap vs overlap/touch

Case A: Overlap

Input: [(540, 600), (570, 660)] i.e., [09:00–10:00), [09:30–11:00)

sorted = [(540,600), (570,660)]init: current=(540,600), total=0step interval (570,660): s=570, currentEnd=600  s > currentEnd? 570 > 600 = false  decision: overlap/touch  currentEnd = max(600,660)=660end loopfinalize: total += (660-540)=120return 120

Case B: Touching intervals (no gap)

Input: [(60, 120), (120, 180)]

sorted = [(60,120), (120,180)]init: current=(60,120), total=0step interval (120,180): s=120, currentEnd=120  s > currentEnd? 120 > 120 = false  decision: overlap/touch (touch)  currentEnd = max(120,180)=180end loopfinalize: total += (180-60)=120return 120

Case C: Gap between intervals

Input: [(60, 90), (120, 150)]

sorted = [(60,90), (120,150)]init: current=(60,90), total=0step interval (120,150): s=120, currentEnd=90  s > currentEnd? 120 > 90 = true  decision: gap  total += (90-60)=30  total=30  current=(120,150)end loopfinalize: total += (150-120)=30total=60return 60

Case D: Unsorted input with nesting

Input: [(300, 360), (240, 480), (360, 420)]

sorted = [(240,480), (300,360), (360,420)]init: current=(240,480), total=0step interval (300,360): s=300, currentEnd=480  s > currentEnd? false  decision: overlap/touch  currentEnd = max(480,360)=480 (unchanged)step interval (360,420): s=360, currentEnd=480  s > currentEnd? false  decision: overlap/touch  currentEnd = max(480,420)=480 (unchanged)finalize: total += (480-240)=240return 240

Case E: Empty and zero-length intervals

Input: []

intervals empty => return 0

Input: [(100,100), (100,130)]

sorted=[(100,100),(100,130)]init current=(100,100), total=0step (100,130): s=100, currentEnd=100  s > currentEnd? false  currentEnd=max(100,130)=130finalize total += (130-100)=30return 30

Deliverable 4: Determinism Check

Use this as a quick audit that the procedure always produces the same output for the same input.

No hidden state: The algorithm uses only sorted, total, currentStart, currentEnd, all derived from the input.
Deterministic ordering: Sorting by a fully specified key (start, then end) ensures the same ordering for the same multiset of intervals.
Deterministic updates: Each step uses deterministic comparisons and MAX.
Deterministic output: The final total is a pure function of the sorted list.

Deliverable 5: Correctness Checklist (Pre/Post + Invariant)

Preconditions (must hold before running)

Each interval is a pair of integers (start, end).
0 ≤ start ≤ end ≤ 1440 for each interval.
Intervals represent half-open ranges [start,end).

Postcondition (must hold after returning)

The returned integer equals the measure (in minutes) of the union of all input intervals under half-open semantics.

Key invariant (maintained during the loop)

Invariant I: After processing the first k intervals of sorted (including initialization as processing the first one), the following are true:

total equals the covered minutes of the union of all completed merged blocks formed from the first k intervals.
[currentStart, currentEnd) equals the union of all intervals among the first k that overlap/touch the current block and have not yet been added into total.
The union of the first k intervals equals (completed blocks counted in total) ∪ [currentStart,currentEnd), and these parts are disjoint.

Why the invariant holds (checklist-style reasoning)

Initialization: Before the loop, total=0 and current is set to the first sorted interval. Completed blocks are none, and the current block equals the union of the first interval. Invariant holds.
Maintenance, gap case (s > currentEnd): There is a strict gap between the current block and the next interval. Because the list is sorted by start, no future interval can start before s, so none can overlap the current block. Adding (currentEnd-currentStart) to total correctly finalizes that block. Setting current to the new interval starts the next block. Disjointness is preserved because of the gap.
Maintenance, overlap/touch case (s ≤ currentEnd): The next interval intersects or touches the current block, so the union of the current block and this interval is still a single block. Updating currentEnd = max(currentEnd, e) makes current represent that union. total remains the union length of completed blocks only, so the partition described by the invariant remains valid.
Termination: After the loop, all intervals have been processed, and the invariant says the union equals (completed blocks counted in total) ∪ current. Adding the final block length completes the union length. This matches the postcondition.

Correctness pitfalls to explicitly rule out

Double-counting overlaps: Prevented because overlapping/touching intervals only extend currentEnd rather than adding their full lengths separately.
Missing coverage: Prevented because every interval either extends the current block or starts a new block that will be finalized.
Touching boundary ambiguity: Resolved by half-open semantics and by using s > currentEnd (not ≥) for a gap.

Reflection Prompt (Draft vs. Verified Procedure)

Compare your first draft of the solution (before writing the deliverables) to the verified procedure above. Answer in writing:

Which phrase(s) in the informal problem statement were ambiguous, and what exact decision did you adopt to remove ambiguity (for example, boundary semantics or validity rules)?
What changed in your algorithm after you wrote trace logs—did any test reveal a missing case or an unclear step?
Where did determinism become explicit (sorting key, tie-breakers, state updates), and what would have been non-deterministic otherwise?
State your invariant in one sentence. How did it force you to clarify what total does and does not include at each step?
If you had to hand this to another person to implement, what is the single most important clarification that prevents a wrong implementation?

Now answer the exercise about the content:

In the interval-union algorithm, why is the gap check written as s > currentEnd (instead of s ≥ currentEnd) when using half-open intervals [start, end)?

You are right! Congratulations, now go to the next page

You missed! Try again.

With half-open intervals [start,end), the end minute is excluded. So when s == currentEnd, there is no gap and no overlap; merging keeps coverage continuous and avoids double-counting.