Unit 5 activity: Verification lab | AI Literacy: Ada, AI, and Verification

DEVELOPMENT REVIEW DEPLOYMENT - NOT READY FOR RELEASE

Time: about 24 minutes. Work through Route A or Route B. They are equal routes and either one completes the unit; do both if you have time, because they catch different things.

Keep everything you write down. It goes into your evidence pack in Unit 8.

Before you start: the safety step

This step belongs to both routes and comes first.

check.py imports and executes the file you give it. Your Unit 4 code came from a source you did not write and have not read. Read it now, before you do anything else, and answer these three questions in writing:

Which modules does it import? A Bernoulli routine needs fractions and possibly math. Anything else needs a reason.
Does anything happen at import time — outside the function body — such as printing, writing a file, opening a network connection, or running a subprocess?
Is there anything you cannot explain? Encoded strings, eval, exec, os.system, or an install command.

If any answer worries you, do not run it. Delete the suspicious part, or switch to Route B, which never executes anything.

Then run it somewhere disposable: a container, a virtual machine, a throwaway account, or at least a directory holding nothing you would mind losing. Not as an administrator.

Route A — Automated verification

A1. Set up (2 minutes)

cd course/lab
python3 reference_bernoulli.py

Confirm the final line reads:

OK: oracle agrees with all 22 published values, odd terms are zero.

If it does not, stop. The oracle is not verified, so nothing you check against it means anything.

A2. Meet the diagnoses (4 minutes)

Run the checker against each supplied wrong example, and against the correct one:

python3 check.py examples/wrong_b1_sign.py
python3 check.py examples/wrong_odd_terms.py
python3 check.py examples/float_output.py
python3 check.py examples/off_by_one_range.py
python3 check.py examples/correct_example.py

Fill in this table from the output before you check the marking guidance below:

file	first divergence at n	expected	got
`wrong_b1_sign.py`
`wrong_odd_terms.py`
`float_output.py`
`off_by_one_range.py`
`correct_example.py`	—	—	—

Then answer in one sentence each:

Why does wrong_odd_terms.py produce two diagnosis codes rather than one?
off_by_one_range.py returns only genuine Bernoulli numbers and contains no arithmetic error. What, exactly, is wrong with it, and why would reading the source not reveal it?

A3. Check your own code (5 minutes)

Put the routine you saved in Unit 4 into the exercise stub, or check it where it is. Either works:

python3 check.py exercises/ex04_bernoulli.py

or, for a file anywhere on your machine:

python3 check.py /full/path/to/your_file.py

Record:

First divergence: at n = ____, expected ______, got ______
Diagnosis code(s): ____________
In your own words, what the fault is: _______

If your file passed on the first run, do not skip ahead. Run it again with the comparison extended and confirm it still passes:

python3 check.py exercises/ex04_bernoulli.py --max-n 40

Then write one sentence saying which clause of the specification your Unit 4 prompt happened to get right by luck rather than by stating it.

A4. Repair (7 minutes)

You have two ways to fix this, and the choice is the interesting part.

Repair the code. Edit the routine directly until the checker passes.
Repair the prompt. Go back to the AI system, add the requirement that was missing, regenerate, and check the new output.

Do at least one. Note which requirement was missing — that observation is exactly what Unit 6 builds on. Then re-run the checker with --verbose until you see:

PASS - agrees with the oracle for every n from 0 to 30,
       returns exact Fractions, and odd terms above B1 are zero.

Passing is not the end of the job. You still have to be able to say
*why* it is correct. That is the Unit 8 defence.

(Indices compared: 0 to 30)

A5. One last question

The checker passed. Write down, in one sentence, something that is still not established about your routine by that pass.

Route B — Table-based verification

This route uses no Python. It performs the same comparison by hand, and it completes the unit on its own terms.

B1. Get the reference values (2 minutes)

Use the reference table in page.md. If you have Python available and want the machine-printed version, python3 reference_bernoulli.py prints the same data, but this is optional here.

B2. Get the generated values (4 minutes)

Go back to the AI system you used in Unit 4 and ask for the values rather than a program:

List the Bernoulli numbers B0 to B12 as exact fractions, and also give B30.

Copy what comes back exactly as it is given, including any decimals. Do not tidy it up. Tidying is where evidence gets lost.

If you have no AI access, use a supplied specimen instead, just as Unit 4 does:

Open course/lab/examples/wrong_b1_sign.py in any text editor. You are reading it, not running it — this route stays code-free.
Its docstring states exactly what the routine returns: it is "correct under the second Bernoulli convention (B1 = +1/2)". So its output table is the reference table with precisely one entry changed: 1/2 at n = 1.
Write that out as your "generated value" column — every reference value unchanged except 1/2 at n = 1 — and carry it into B3.

B3. Compare in index order (6 minutes)

Write the two columns side by side, in index order, and go down the rows.

n	reference value	generated value	same?
0	1
1	-1/2
2	1/6
3	0
4	-1/30
5	0
6	1/42
7	0
8	-1/30
9	0
10	5/66
11	0
12	-691/2730
30	8615841276005/14322

Stop at the first row that differs. That is the first divergence, found by hand, using the same method the tool uses. Record it:

First divergence: at n = ____
Which named failure mode does it match? Use the table in page.md.

Then check three things that are easy to miss when scanning:

Are the odd rows present and exactly 0, or are they missing, or "about zero"?
Are the values exact fractions, or decimals such as -0.0333?
Did B30 come back at all, and is it exactly 8615841276005/14322?

B4. Repair (6 minutes)

Go back to the AI system, state the requirement that was missing, and ask again. Compare the new table against the reference the same way. Record which single sentence you added and what changed.

If you have no AI access, treat a second supplied specimen as the "regenerated" attempt:

Open course/lab/examples/wrong_odd_terms.py and read its docstring — again without running anything.
Build its output column from what the docstring states: the routine renumbers the non-zero terms consecutively, so its bernoulli(k) is the modern B(2k). Its column therefore reads 1 at n = 0, then 1/6, -1/30, 1/42, -1/30, 5/66 at n = 1 to 5.
Compare that column against the reference exactly as in B3, in index order, and record the first divergence.
Instead of the sentence you added, record the single sentence a repair prompt would need for this specimen — the requirement its docstring says it violates.

B5. One last question

Your two tables now agree. Write down, in one sentence, why that does not establish that a program produced those values.

B6. Check what the table evidence supports (4 minutes)

Open cp05-table-evidence in the browser self-check. It gives four observations from manual candidate/reference table comparisons. Match each observation to the strongest conclusion it supports.

This is the browser-assessable counterpart to the executable checkpoint, not a simulation of running code. It checks modern indexing, zero odd terms, exact displayed values, first-convention handling, and the boundary of manual evidence. A matching table supports the cells compared; it does not establish the return type of unseen code, unlisted indices, or that a program produced the table.

Finish the unit at the checkpoints

The checkpoints are formative and unmarked. cp05-diagnose is shared. cp05-table-evidence records the manual evidence objective on Route B. cp05-bernoulli runs check.py against a file and belongs to Route A. The two route-specific checkpoints test the same contract with honestly different coverage.

Python route — from course/lab:

python3 selfcheck.py run cp05-bernoulli
python3 selfcheck.py run cp05-diagnose

To practise both routes, including the table-evidence checkpoint, run the whole unit:

python3 selfcheck.py run --unit 5

Browser route — open build/site/selfcheck.html in any browser, with no installation, and answer cp05-table-evidence and cp05-diagnose. The browser self-check cannot run code, so it cannot grade cp05-bernoulli; it lists that checkpoint and directs you to complete it in the Python lab.

cp05-bernoulli requires a completed exercises/ex04_bernoulli.py; until you edit the stub it will report that the checkpoint has not been attempted rather than failing you.

To see where you have got to:

python3 selfcheck.py list
python3 selfcheck.py progress

Explore, if you want to

The oracle is there to be poked at, not only to judge you:

python3 selfcheck.py explore

Inside, b 30 prints B30 exactly, float 30 shows the exact value and the float side by side, table 20 prints a range, map shows the Note G index mapping, check <file> runs the checker, and quit leaves.

Optional CS extensions

Optional. These are outside the core study time and are not required to complete this unit or the module. Non-programmers lose no core content by skipping them.

Write the test yourself — exercises/ex05_write_a_test.py

python3 exercises/ex05_write_a_test.py

So far the checker has done the judging. Here you write it: a single function that must separate four supplied faulty implementations from one correct one, without wrongly rejecting the correct one. A test that only checks B4 == -1/30 lets two of the four straight through. The exercise grades itself against the real files in examples/ and tells you which you caught and which you missed.

Translate between Ada's indexing and ours — exercises/ex06_ada_translation.py

python3 exercises/ex06_ada_translation.py

Implement the mapping from Lovelace's Note G labels to modern indices, returning exact values and rejecting indices that have no Note G label at all. This one looks ahead to Unit 7; you can do it now or after that unit.

Marking guidance — open this once you have done the activity, to check your own work

Answer key for the Unit 5 activity. Self-check checkpoints are not answered here; they mark themselves and give their own diagnostic feedback, by either route.

Read this after attempting the activity. Where a question asks for your own routine, the key describes what a good answer looks like rather than giving one.

Before you start — the safety step

There is no single right answer, but there is a right shape of answer.

Imports. fractions is expected; math is reasonable, usually for comb. Anything else needs a reason you can state. os, sys with path manipulation, socket, subprocess, urllib, requests, shutil and pathlib writes have no place in a routine that computes a number from an integer.
Import-time behaviour. Anything outside a function body runs the moment the checker imports the file. A print is harmless and untidy; a file write, a network call or a subprocess is neither. Note that a if __name__ == "__main__": block does not run on import, so a demonstration loop there is fine.
Unexplained code. The honest answer is often "I could not tell what this line does". That is a finding, not a failure. Code you cannot read is code you cannot vouch for, and the correct response is to remove it or not run it.

A learner who reports "nothing suspicious, here is why" with specific reasons has done this correctly. A learner who reports "it looked fine" has not done it at all.

A2 — The supplied examples

Exact figures from the checker, at the default --max-n 30:

file	first divergence at n	expected	got	diagnosis code(s)
`wrong_b1_sign.py`	1	`-1/2`	`1/2`	`b1-sign`
`wrong_odd_terms.py`	1	`-1/2`	`1/6`	`odd-terms`, `ada-indexing`
`float_output.py`	2	`1/6`	`0.16666666666666674`	`not-fraction`, `odd-terms`
`off_by_one_range.py`	0	`1`	`-1/2`	`off-by-one`, `odd-terms`
`correct_example.py`	—	—	—	none; PASS

Notes on the details that catch people out:

The [divergence] line is not itself a named failure mode. It locates the fault; the codes classify it. A report normally contains both.
float_output.py is reported as not-fraction "first seen at n=0", because even B0 = 1.0 is already the wrong type, while the first value divergence is at n=2. Type and value are separate failures and are found by separate checks.
off_by_one_range.py picks up odd-terms as well, because shifting the sequence moves the non-zero even values onto odd indices. One underlying fault, two violated requirements.

Why does wrong_odd_terms.py produce two codes? Because one mistake breaks two separate requirements. Renumbering the non-zero terms consecutively means the odd indices no longer hold zero (odd-terms), and it also means every label names a different number from the modern one (ada-indexing — though these are not Lovelace's labels either; hers run B1, B3, B5, B7 = modern B2, B4, B6, B8). A diagnostic system that reported only the first symptom would leave you fixing half the fault.

What is wrong with off_by_one_range.py? Every value it returns is a genuine Bernoulli number, and every one is filed under the wrong index: its bernoulli(0) hands back B1, its bernoulli(4) hands back B5. Reading the source does not reveal it because there is nothing badly written to see — the arithmetic is exact, the style is clean, and the values are all real. The fault is a relationship between the code and a reference outside the code, and only a comparison against that reference exposes it. This is the strongest argument in the unit for differential testing over code review.

A3 — Your own code

A good record is specific:

First divergence at n = 1, expected -1/2, got 1/2. Diagnosis: b1-sign. The routine implements the second Bernoulli convention; my prompt never said which convention I wanted, so the specification was incomplete rather than the code being wrong.

Common outcomes, and what each tells you about the prompt that produced them:

diagnosis	what the prompt failed to state
`b1-sign`	which Bernoulli convention to use
`odd-terms`	that odd indices above 1 must return exactly zero
`ada-indexing`	that modern indexing is required, not Note G's
`off-by-one`	the value at named indices, anchoring where the sequence starts
`not-fraction`	that returns must be exact `fractions.Fraction`, never `float`
`raises`	that the function is defined for every `n >= 0`
`no-function`	the required function name and signature
`import-error`	that the module must import cleanly using only the standard library

If it passed first time, the honest answer names the clause you got for free. Typically it is exact arithmetic — a request phrased around Ada Lovelace or exact values sometimes yields Fraction without being asked, and sometimes does not. Getting it without asking is luck, and luck is not a property you can rely on next time. That observation is the whole of Unit 6 in one line.

A5 — what the pass does not establish. Any of these is a good answer:

That the routine is correct for n > 30, or for n > 40 if you extended the comparison. The check is finite.
That the convention it agrees with is the one your actual task requires. It agrees with this module's oracle.
That you understand it, or could reproduce or repair it.
That any comment in the file is true. Comments are not executed and are not checked.
That the code is safe to run on data other than integers, or free of performance problems at large n.
That the algorithm is the one you claimed to use.

B3 — Table route

The first divergence found by hand is the same index the tool would report, provided you compared in index order and stopped at the first difference. If you scanned for "the obviously wrong one" instead, you may have found a later divergence that is only a consequence of an earlier one.

The three things that are easy to miss when scanning:

Odd rows. Many generated tables omit the odd indices entirely, listing only B0, B1, B2, B4, B6, .... An omitted row is not the same claim as a row containing zero, and the difference matters: the specification requires bernoulli(3) to return zero, not to be undefined. If the odd rows are present but written as 0.0, ~0 or 1e-17, that is the float failure mode.
Exact fractions. -0.0333... is not -1/30. It is close, and closeness is the property the specification rules out. Any decimal at all is a not-fraction finding.
B30. A table that agrees perfectly from B0 to B12 and then gives 601580873.9 or 6.0158e8 for B30 has told you exactly what you needed to know. If B30 was refused or omitted, treat that as unverified rather than as correct.

B5 — why agreement does not establish that a program produced the values. A table in a chat window is generated text. It may have been produced by a routine, copied from a published table, or generated the same way as any other text. Those are different claims with different reliability, and the table looks identical in all three cases. The values being right tells you the values are right; it tells you nothing about the existence or behaviour of a program. If your task requires a working routine, that is a separate claim needing separate evidence — which is what Route A supplies.

Marking the two routes

Both routes evidence the same skill: ordered comparison against a trusted reference, stopping at the first divergence, and naming the fault. A learner who completed Route B has verified. Do not treat Route A as the real version.

The distinguishing feature of a good submission by either route is specificity: an index, a pair of values, a named failure mode, and a sentence about which requirement was missing. "It was wrong and then I fixed it" is not a verification record.

Optional CS extensions

These are optional and outside the core study time. Do not treat them as required.

ex05_write_a_test.py. The exercise grades itself, so no key is given here. The instructive failure is a test that catches all four faulty implementations by being aggressive and then wrongly rejects correct_example.py — the file reports that separately, and says why it is worse than missing a fault: a test that fails good code is a test people learn to ignore. The second instructive failure is a test built from == against a handful of known values, which lets the type-related and range-related faults through. A test that works generally checks a property and a type, not only a list of values.

The point to draw out afterwards: every clause the learner needed in their test corresponds to a clause the specification should have contained. That list is the one they build in Unit 6.

ex06_ada_translation.py. Also self-grading. Note that the exercise requires rejecting Ada B2 and Ada B0 with a ValueError, not only computing Ada B7 correctly. Learners often implement the mapping and forget the rejection, and the exercise says why that matters: a translation layer that silently accepts nonsense from the other side is how convention bugs travel between systems.

Checkpoints

cp05-bernoulli, cp05-table-evidence, and cp05-diagnose are self-marking, with their own diagnostic feedback, and their answers are deliberately not reproduced here. Learners reach cp05-diagnose by either route; cp05-bernoulli belongs to the Python route and cp05-table-evidence to the browser/table route:

python3 selfcheck.py run cp05-diagnose     # or use the browser self-check
python3 selfcheck.py run cp05-bernoulli    # Python route only
python3 selfcheck.py run cp05-table-evidence  # table route; browser or CLI

Your private activity record

Browser storage is not a permanent copy

Progress is kept only in this browser, profile and device. Private browsing, clearing site data, removing the profile, a browser reset, storage eviction or device loss can erase it. Keep important answers and contributions separately.

Your answers and working notes

These notes stay in this browser unless you download a backup or activity log.

I have attempted this activity and reviewed its guidance.