Ad argvmentvm transi
Topos Uranos
Latine

Temptare

Svmmarivm

Programma qvod compilatvr et aliqvid verisimile scribit non ideo temptatvm est. Haec lectio docet methodo temptare: casvs ex specificatione dedvcere, per regiones et margines; eos in programma tentaminvm avtomaticorvm colligere qvod defectiones nvmerat et nvntiat; per assert examinare qvod accidere non potest si programma rectvm est, et per static_assert, dvm compilatvr, qvod fvnctio constexpr compvtare debet; et tentamina cvm detectoribvs exseqvi, qvi modvm agendi indefinitvm detegvnt qvem eventvs rectvs celat. Omnia vni admonitioni innitvntvr: tentamen praesentiam erroris ostendere potest, nvmqvam absentiam.

Proposita discendi

  1. Casvs tentaminis ex specificatione fvnctionis dedvcere: partitiones eivs introitvs, margines inter eas et casvs singvlares, cvm eventv qvem postcondicio in qvoqve exigit.
  2. Programma tentaminvm avtomaticorvm scribere qvod eventvs obtentos cvm exspectatis comparet, qvamqve defectionem nvntiet nec sistat, et svmmario ac nvmero terminationis id reddente finiatvr.
  3. assert adhibere ad praecondiciones et invariantes examinandas, et explicare cvr evanescat cvm -DNDEBUG compilatvr et cvr eivs condicio effectvs secvndarios habere non debeat.
  4. static_assert cvm fvnctionibvs constexpr adhibere ad eventvs dvm compilatvr temptandos, et tentamina cvm detectoribvs exseqvi ad modvm agendi indefinitvm detegendvm qvem eventvs non revelant.

Qvid sit temptare

Temptare programma est id cvm introitibvs electis exseqvi et comparare qvod facit cvm eo qvod facere debebat. Qvisqve casvs tentaminis dvobvs membris constat: introitv qvi praecondicioni satisfacit, et eventv qvem postcondicio pro eo exigit, antea et alia via compvtato (manv, alia formvla, tabvla nota). Sine eventv exspectato non est tentamen, sed exsecvtio tantvm: exitvm inspicere evmqve «verisimilem» invenire impressio est, non comparatio.

Iam vero fvnctio vnivs argvmenti int plvs qvam qvattvor milliarda introitvvm admittit, et fvnctio dvorvm argvmentorvm circiter 1,8⋅10191{,}8 \cdot 10^{19} paria; nvlla series tentaminvm omnia percvrrit. Qvod si ita est, tentamina minimam portionem casvvm possibilivm examinant, et ex eo qvod omnia transevnt non seqvitvr fvnctionem rectam esse. Edsger Diikstra id anno 1970 formavit: tentamina praesentiam errorvm ostendere possvnt, nvmqvam absentiam. Distinctio ea est qvam cvrsvs Logica Mathematica I inter casvs verificandos et demonstrandvm statvit: verificare formvlam pro qvibvsdam valoribvs veram esse non demonstrat eam pro omnibvs veram esse, dvm demonstratio (in hoc cvrsv, invarians lectionis Circvitvs rectos designare) omnes casvs simvl complectitvr. Tentamina hanc ratiocinationem non svpplent: errores invenivnt qvos ea praetermisit.

Hinc seqvitvr regvla casvs eligendi. Si tentamina rectitvdinem confirmare non possvnt, eorvm pretivm in erroribvs inveniendis est, et bonvs casvs tentaminis is est qvi maxime verisimiliter deficiet. Casvs electvs qvia sciebatvr evm recte cessvrvm esse nihil indicat. Programma seqvens id ostendit fvnctione qvae maximvm elementvm vectoris non vacvi reddere debet.

Programma in C++
#include <print>#include <vector>​// Maximvm elementvm catalogi datorvm.// Praecondicio: values vacvvm non est.// Postcondicio: reddit maximvm elementvm ex values.int largest(const std::vector<int>& values){    int best{0};    for (const int v : values) {        if (v > best) {            best = v;        }    }    return best;}​int main(){    std::println("{}", largest({3, 9, 4}));    std::println("{}", largest({7}));    std::println("{}", largest({1, 2, 3, 4}));    std::println("{}", largest({-5, -2, -8}));}
Exitvs
9740

Tres primi casvs ii svnt qvos qvilibet primos scribit, et fvnctio eos transit: 9, 7 et 4 recti svnt. Qvartvs 0 dat, valorem qvi ne in vectore qvidem est, cvm −2-2 dare deberet. Error in versv 9 est: best a 0 incipit, non a primo elemento, ita vt fvnctio recta sit solvm si aliqvod elementvm positivvm vel zero est. Casvs typici hanc proprietatem commvnem habebant, nemine eam eligente; qvartvs eam consvlto violat. Correctio est int best{values[0]};, qvam praecondicio legitimam reddit, qvia praestat values[0] exstare.