Hic articulus est translatio . Sed paulo ante eam introductio. Quomodo zombies formatur? Omnes in condicionem venerunt ubi amicum aut collegam volunt ad suum gradum trahere, sed non elaborare. Et non tam apud te quam cum illo quod "non operatur": in una parte scalae salarium normale, negotium, et sic porro, et in alia, necesse est cogitare. Cogitatio ingrata est et molesta. Celeriter recedit et codicem scribere pergit sine conversione in cerebro suo omnino. Quantum molis cogitas doctarum inopiam superare impedimentum, quod non facis. Ita fiunt immortui, quod videtur sanari posse, sed videtur quod nemo faciet.
Cum vidi quod (ita, idem comes e tradenda) et non relationem, sed interrogationem et responsionem, parum cautus fui. Sicut in casu Leslie est clarissimus physicus, auctor operum fundamentalium in computando distribuendo, et etiam per litteras La in verbo LaTeX - "Lamport TeX" cognoscere potes. Alter factor terroris postulatio est: omnis qui venit, debet (absolute gratis) audire duas relationes suas in praemissis, cum una saltem quaestione super eas ascendat et tunc demum veniat. Placui videre quid Lampor iaciebatur ibi - ac suus magnus! Hoc ipsum est, lobortis ligamentum magicum ad zombies sanandum. Moneo te ex textu, amatores methodologiarum super- flexibilium, et qui non placent probare quod scriptum est, notabiliter deflagrare possunt.
Post habrokat re vera incipit translatio Seminarii. Fruere legendo!
Quidquid moliris, semper debes ire per tres gradus;
- quid vis consequi metam;
- constitue quomodo propositum consequeris;
- ad propositum tuum.
Etiam id vestibulum est. Cum scribimus codicem, necesse est nos;
- quid institutum faceret;
- determinare debet quomodo suum munus expleat;
- correspondentes scribe in codice.
Extremum sane momenti est, sed hodie non loqui. Sed de primis dicemus. Omnis programmator ea praestat antequam ad laborem proficiscatur. Scribere non discumbere nisi decreveris utrum navigatrum vel datorum scribas. Idea quaedam finis debet esse praesens. Et tu plane cogita quidnam rem agendi ratio facturus sit, nec aliquo modo scribe in eo sperans codicem aliquo modo in pasco convertturum.
Quam exacte hoc signum prae-cogitandi fiet? Quantum moliendum est in hoc? Refert quam implicatam quaestionem solvimus. Esto: vis distributa ferendum culpa scribenda ratio. In hoc casu omnia diligenter cogitare debemus antequam ad codicem consedimus. Quid si tantum indigemus incremento integer variabilis per 1? Primo aspectu, omnia hic levia sunt, et nulla cogitatio opus est, sed tunc meminimus fieri posse redundantiam. Ergo, ut intelligas utrum quaestio simplex sit an multiplex, primum cogitare debes.
Si cogitas solutiones possibilium problematis in antecessum, errata vitare potes. Sed hoc postulat ut cogitatio tua clara sit. Ad hoc assequendum debes cogitationes tuas scribere. Ego vere amo Dick Guindon refert: βCum scribis, natura tibi ostendit quam imperitis cogitatio tua sitβ. Si non scribis, tantum cogitas te cogitare. Et debes cogitationes tuas scribere in forma specificationum.
Specificationes multa munera exercent, praesertim in magnis inceptis. Sed tantum de uno eorum loquar: adiuvant ut clare cogitemus. Evidenter cogitandum est magni ponderis et satis difficilis, ergo hic omni ope indigemus. Qualem linguam scribere debeamus specificationes in? In genere semper haec est prima quaestio programmatoribus: qua lingua scribemus. Non est qui recte respondeat: problemata quas solvimus nimis sunt diversae. Aliquot TLA + specificatio est lingua quam elaboravi. Aliis commodius est uti Sinica. Omnia ex situ pendent.
Gravior alia quaestio est: quomodo clarius cogitandum assequendum? Respondendum est: Putare debemus ut docti. Haec est modus cogitandi quae per praeteritum 500 annos se probavit. In scientia figuras rerum mathematicas construimus. Astronomia fortasse prima scientia proprie vocabuli fuit. In exemplari mathematico astrologiae adhibito, corpora caelestia apparent puncta cum mole, positione et momento, quamvis sint objecta valde complexa cum montibus et oceanis, aestus et aestus. Hoc exemplar creatum est ut quaelibet alia problemata solvenda. Multum est diiudicare ubi telescopium designare si planetam invenire debes. Si autem tempestates in hac tellure praedicere vis, hoc exemplum non operabitur.
Formae proprietates Mathematicae nobis permittunt determinare. Et ostendit scientia quomodo praedictae proprietates ad rem pertinent. Loquamur de scientia nostra, de scientia computatrum. Res, qua laboramus, systemata varii generis computant: processus, lusus consolantur, computatores, programmata exsequendi et cetera. Loquar de programmate computatorio, sed et magno, omnes hae conclusiones ad quamlibet rationem computandi pertinent. In scientia nostra multa exempla varia utimur: Machina Turinga, rerum gestarum partim ordinata, et multa alia.
Quid programma est? Hic est in quolibet codice qui independenter considerari potest. Puta navigatrum scribere necesse est. Tria opera facimus: sententiam utentis programmatis designamus, tum summus gradus schematis programmatis scribimus, denique codicem scribimus. Cum scribimus codicem, intellegimus nos formare textum scribere necesse esse. Hic iterum tria problemata solvenda oportet: determinare quid hoc instrumentum in textum revertatur; algorithm pro formatting eligere; codicem scribere. Hoc negotium suum subtilitatem habet: recte hyphen in verba. Solvimus etiam hoc negotium in tribus gradibus - ut vides, in multis gradibus repetuntur.
Primum gradum planius consideremus: quam quaestionem solvit propositum. Hic saepissime exemplar programma pro functione quae aliquid initus sumit et aliquid output producit. In mathematicis, functio consueta describi solet paria esse ordinata. Exempli causa, munus quadratura pro numeris naturalibus describitur {<0,0>, <1,1>, <2,4, <3,9>, β¦}. Regio talis functionis est prima elementa cuiusque par, id est numeri naturalis. Ad functionem definiendam, eius scopum et formulam definire oportet.
Sed munera in mathematicis non eadem sunt ac munera in programmatibus linguarum. Math multo facilius. Cum exemplum complexuum non vacat, simplicem consideremus: functionem in C vel methodo stabili in Java quae maximum divisorem duorum integrorum reddit. In specificatione huius methodi scribemus: calculat GCD(M,N) pro argumentis M ΠΈ Nquibus GCD(M,N) - functio cuius dominium est numerus parium integrorum, et reditus valor maximus integer qui divisibilis est M ΠΈ N. Quomodo hoc exemplar ad rem pertinet? Exemplar in integris operatur, dum in C vel Java habemus 32-bit int. Exemplar hoc nobis permittit decernere si algorithmus recte est GCDsed errores redundare non prohibebit. Hoc exemplum implicatius egeret, ad quod tempus non est.
Fama de limitibus functionis tamquam exemplar. Aliquot programmata (ut systemata operandi) certum valorem certarum argumentorum non solum reddere, continue currere possunt. Praeterea munus exemplar pro secundo gradu non bene convenit: ratio solvendi quaestionem. Celeres modi et bullae huiusmodi eandem functionem computant, sed algorithmorum omnino diversae sunt. Ut igitur describam quomodo propositum progressionis obtineat, alio utar exemplo, illud modalis morum exemplar vocemus. Propositum in eo repraesentatur ut omnium licitorum morum institutio, quarum singulae vicissim sequela statuum est, et status valorum variabilium assignatur.
Videamus quid secundus gradus ad Euclidem algorithmum spectare velit. Non opus est calculare GCD(M, N). Nos initialize M quam xquod N quam ytunc minora ex his variabilibus a majoribus identidem minue, donec aequalia sint. Exempli gratia, si M = 12quod N = 18, sequentes mores describere possumus;
[x = 12, y = 18] β [x = 12, y = 6] β [x = 6, y = 6]
Et si M = 0 ΠΈ N = 0? Nulla est divisibilis per omnes numeros, ergo nullus est maximus divisor in hoc casu. In hoc situ, ad primum gradum revertamur et quaeramus: num revera opus est GCD pro numeris non-positivis computare? Si hoc non est necessarium, solum debes mutare speciem.
Hic de fructibus parvam digressionem debemus facere. Saepe mensuratur in numero versuum codicis per diem scriptum. Sed opera tua multo utilius est si certos lineas removeas, quia cimices minus capias. Atque in primo gradu codicis carere facillimum est. Omnino fieri potest ut non opus sit omnibus campanis et sibilis, quem efficere conaris. Velocissima via est ad simpliciorem rationem programma ac tempus conservandum est non facere quae non debent fieri. Secundus gradus est secundus potentia salutaris temporis. Si fructibus in terminis scriptis metiaris, tunc cogitas quomodo opus perficiendum te efficiet minus fructuosapropterea quod eandem quaestionem minori codice solvere potes. Hic statisticas exigere non possum, quia numerus linearum numerare nullo modo possum quos non scripsi ex eo quod de specificatione, hoc est in primis et secundis gradibus, tempus consumpsi. Et experimentum hic vel non erigi potest, quia in experimento non habemus ius absolvendi primum gradum, negotium praefinitum est.
Facile est multas difficultates praeterire in specificationibus informaticis. Non est hoc difficile in scribendo stricte notationes ad functiones. Sed loquemur de notionibus fortibus scribendo ad mores normae. Theorema est quae dicit omnem modum agendi describi posse utens res securitatis (salus) ac survivability possessiones (vivit). Securitas significat nihil mali futurum esse, propositum responsum non recte dabit. Survivability significat quod citius vel serius aliquid boni fiet, i.e. ratio rectam responsum citius aut serius dabit. Pro regula, securitas maioris momenti indicatio est, errores hic saepissime occurrunt. Ergo ad tempus conservandum, non de superstite loqui, licet, scilicet, etiam maximus.
Securitatem consequimur praecipiendo primo statutis initialibus possibilium. Secundo, relationes cum omnibus proximis civitatibus ad quemlibet statum possibilium. Ut phisicis agamus, et res mathematice definias. Status status initialis describitur per formulam, v. gr. in casu Euclidis algorithmi; (x = M) β§ (y = N). Nam quaedam values M ΠΈ N unus est tantum status initialis. Relatio cum proximo statu describitur per formulam in qua variabiles status sequentis cum primario scribuntur, et variabiles status hodierni sine prima scripta sunt. In algorithmo Euclidis agemus de disjunctione duarum formularum, quarum altera. x maximum valorem, et in secundo - y:
In primo casu, novus valor ipsius y priori valori ipsius y est aequalis, et novum ipsius x valorem obtinemus, subtrahendo minorem variabilem ex variabili maiore. In secundo casu contrarium facimus.
Ad Euclidis algorithmum revertamur. Demus iterum quod M = 12, N = 18. Hoc unum initiale definit; (x = 12) β§ (y = 18). Nos igitur valores illos plug in formulam superius et accipimus:
Hic est sola solutio; x' = 18 - 12 β§ y' = 12et mores obtinemus; [x = 12, y = 18]. Similiter omnes status in moribus nostris possumus describere; [x = 12, y = 18] β [x = 12, y = 6] β [x = 6, y = 6].
In ultimo statu [x = 6, y = 6] utra- que locutio falsa erit, sic deinceps status non habet. Itaque perfectam speciem secundi gradus habemus - ut vides, haec mathematica est admodum ordinaria, sicut in mechanicis et phisicis, et non mirum, sicut in scientia computativa.
Hae duae formulae in unam formulam logicae temporalis componi possunt. Elegans et facilis est ad explicandum, sed tempus non est ei nunc. Temporalem logicam tantum indigere ad vivacitatem rerum, non ad securitatem. Non amo logicam temporalem ut sic, mathematica non est omnino ordinaria, sed in rebus vitae est malum necessarium.
In algorithm Euclidis pro quolibet valore x ΠΈ y habere unique values x' ΠΈ y'quae relationem cum proximo statu faciunt. Id est, algorithmus Euclidis est deterministicus. Ad algorithmum non-deterministicum exemplar, status hodiernus debet habere plures status futuros possibiles, et quodlibet immensus variabilis valor habet plures formas variabiles, ita ut relatio ad statum proximum verum sit. Hoc facile est, at exempla nunc non dabo.
Ut instrumentum operarium, mathematica formali opus est. Quomodo specificatio formalis? Ad hoc opus formale lingua, e.g. . Specificatio algorithmi Euclidis hoc in lingua hac spectare videtur:
Signum aequale signum cum triangulo significat valorem laevae signi definiri aequalem esse valori ad dextram signi. Essentialiter definitio est definitio, apud nos duae definitiones. Ad specificationem in TLA+, declarationes quaedam et syntaxin addere debes, sicut in lapsus supra. In ASCII hoc spectare videtur:
Ut vides, nihil implicatum est. Specificatio pro TLA + probentur, i.e., omnes mores possibilis in parvo exemplari praeterire. In casu nostro, hoc exemplar valores quidam erunt M ΠΈ N. Haec methodus verificationis efficax et simplex est omnino latae. Potest etiam scribere rationes veritatis formales easque mechanice coercere, sed hoc multum temporis, sic fere nemo hoc facit.
Praecipuum incommodum TLA+ est quod math est, et programmatores et phisici computatrum math timent. Primo aspectu, hoc ioco sonat, sed, proh dolor, in omni gravitate intelligo. Collega meus modo narrabat quomodo TLA+ pluribus tincidunt explicare conatus est. Ut primum formulae in velo apparuerunt, illico oculi vitrei facti sunt. Si TLA + te terret, uti potes , genus programmationis ludibrii est. Expressio in PlusCal potest esse quaevis expressio TLA+, id est, per et magna, quaevis dictio mathematica. Praeterea PlusCal syntaxin pro algorithms non-deterministicis habet. Quia PlusCal scribere potest quamlibet expressionem TLA+, PlusCal multo expressius quam aliqua lingua programmandi reali. Deinde, PlusCal in specificatione facile legibili TLA+ exaratum est. Hoc non significat, utique, speciem complexum PlusCal in simplicem convertet in TLA + β modo perspicuum est inter eos correspondentia, nulla implicatio additae erit. Denique haec specificatio per instrumenta TLA+ verificari potest. Omnino PlusCal auxilium mathematicam phobiae vincere potest et facile est intellegere etiam programmatibus et phisicis computatris. Olim algorithms in ea aliquamdiu (circa 10 annos) edidi.
Obiiciet fortasse aliquis TLA + et PlusCal mathematica esse, et mathematica tantum in exemplis inventis operari. Re vera lingua cum typis, processibus, obiectis debes, et sic porro. Hoc nefas est. Hic est quod Chris Newcomb, qui apud Amazonium laboravit, scribit: "TLA+ in decem maioribus inceptis usi sumus, et in unaquaque causa notabilem differentiam ad evolutionem fecit quod cimices periculosos capere potuimus antequam productionem attingeremus, et quod prudentiam et confidentiam nobis dabat operam ut incrementa faceret optimizations non afficiens veritatem progressionis". Saepe audire potes quod, adhibitis rationibus formalibus, codicem inutilem accipiamus - in praxi, omnia prorsus contraria sunt. Praeterea opinatur dispensatores non posse convinci de necessitate methodorum formalium, etiamsi programmatores de eorum utilitate convincantur. Scribit et Nov. "Procuratores nunc difficiles sunt ad scribendas specificationes pro TLA +, et specialiter tempus collocant huic". Cum ergo actores videre TLA+ laborat, laeti sunt eam accipere. Chris Newcomb hoc scripsit ante sex menses (October 2014), nunc autem, quantum scio, TLA+ in 14 inceptis adhibetur, non 10. Aliud exemplum est in consilio Xbox 360. Internus venit ad Carolum Thacker et memoriae ratio scripsit nominationem. Propter hanc speciem, cimex repertum est quod alioqui lateret, et ob id quod omne Xbox 360 collideret post quattuor horarum usus. IBM fabrum confirmavit eorum probationes hanc cimex non invenisse.
Plura de TLA + in Interrete legere potes, sed nunc de speciebus informaticis fama est. Raro habemus scribere programmata quae minimum divisorem commune et similia computant. Multum saepius programmata scribimus sicut instrumentum pulchre typographi quem scripsi pro TLA+. Post processus simplicissimus, TLA + signum hoc simile esset:
Sed in exemplo superiore, uter fere voluit coniunctionem et signa aequalia perpendenda esse. Recta igitur forma hoc magis placet;
Considerans lets 'quoque pro exemplo:
Hic e contra, alignment parium, additionis, et multiplicationis signorum in fonte temere fuit, sic processus simplicissimus satis est. In genere nulla est definitio mathematicae accuratae recte formatting, quia "recte" in hoc casu significat "quod utens vult", quod mathematice determinari non potest.
Videtur quod si non habeat definitionem veritatis, frustra specificatio. Etiam sed fringilla nisi. Quia nescimus quid programma faciendum putetur, non oportet cogitare quomodo operatur, immo magis laborandum est. Specificatio maxime momenti hic est. Impossibile est optimam rationem typis imprimendi definire, sed hoc non est quod omnino non accipiamus, et scribens codicem tamquam rivus conscientiae non est bonum. In fine scripsi specificationem sex regularum cum definitionibus in forma comment in file Java. Exemplum est unius regulae: a left-comment token is LeftComment aligned with its covering token. Haec regula in mathematicis Anglicis dicemus; LeftComment aligned, left-comment ΠΈ covering token β crat definitiones. Sic mathematici mathematicam scribunt: diffinitiones nominum scribunt et ex eis regulas. Talis specificationis utilitas est ut sex regulas multo facilius ad intellegendum et debug quam 850 lineas codicis facilius sint. Has regulas scribere non facile fas fuit, sed multum temporis ad ea debug. Praesertim ad hoc codicem scripsi, qui retulit qua regula usus est. Propter quod in pluribus exemplis has sex regulas probavi, 850 lineas codicis non habui, et cimices evasit ut facile invenias. Java instrumenta magna pro hoc habet. Si modo scripsissem codicem, multo diutius me ademisset, deterioris forma fuisset.
Cur formalis specificatio adhiberi non potuit? Ex altera parte, recta executio hic non est magni momenti. Printouts structural nulli placere tenentur, quare eam non habui in omnibus adiunctis imparibus recte operari. Etiam maius est quod instrumenta idonea non habui. Exemplar tessellatum TLA+ hic inutile est, ideo exempla manually scribere velim.
Haec specificatio notas habet communes omnibus specificationibus. Altior est quam in codice. Lingua quavis impleri potest. Instrumenta quaevis seu methodi scribendi inutiles sunt. Nulla programmatio cursus adiuvabit ut hanc speciem scriberes. Nec desunt instrumenta quae specificationem hanc non necessariam reddere possint, nisi forte linguam specialem scribis scribendo programmata impressa in TLA+. Denique haec specificatio de re prorsus non dicit quomodo codicem scribemus, id solum declarat quid sit signum. Nos nominationem scribimus adiuvare nos cogitare per problema antequam incipimus de codice cogitare.
Sed haec specificatio etiam notas habet quae ab aliis specificationibus distinguuntur. 95% aliarum specierum signanter breviores et simpliciores sunt;
Praeterea, haec specificatio regulae ponitur. Pro regula, hoc signum est specificationis pauperum. Intellectus consequentiae regulae statuto satis difficilis est, quam ob rem multum temporis debugging eas consumere. Sed in hoc casu melius invenire non potui.
Operae pretium est pauca dicere de programmatibus quae continenter currunt. Pro regula operantur in parallelis, exempli gratia, systemata operandi vel systemata distributa. Pauci admodum possunt ea mente vel charta intelligere, et non sum unus, tametsi semel id facere potui. Ideo nobis opus est instrumentis quae opus nostrum reprimunt, exempli gratia, TLA + vel PlusCal.
Cur necesse erat specificationem scribere, si iam scirem quidnam signum faceret? Nam ego tantum sciebam. Praeterea, cum specificatione, extraneus non iam indiget ut in codice ad cognoscendum quidnam faciat. Regulam habeo: generales nullae sint regulae. Excipitur huic regulae, scilicet, unicam regulam generalem sequor: nominatio quid in codice facit, indicet homines omnia quae scire debent cum codice utendo.
Quidnam igitur programmers scire opus est de cogitando? Imprimis, idem quod ceteri omnes: si non scribis, id solum tibi videtur quod cogitas. Item, debes cogitare ante codicem, id quod debes scribere ante codicem. Specificatio est quae scribimus antequam coding incipiamus. Specificatio necessaria est ad quemlibet codicem, qui ab aliquo adhiberi vel mutari potest. Et hic "quis" potest esse ipsius codicis auctor mensem postquam inscriptus est. Specificatio necessaria est ad magnas rationes et systemata, ad classes, ad methodos, interdum etiam ad sectiones complexas unius methodi. Quidnam de codice scribi debet? Describere debes quid agat, id est quid utile alicui homini hoc codice utens. Nonnumquam etiam opus est definire quomodo codicem suum finem perfecerit. Si per hanc methodum in algorithms ambulavimus, algorithm vocamus. Si aliquid specialius et novum est, tunc consilium altam vocamus. Nulla hic differentia formalis est: utrumque exemplar abstractum progressionis.
Quam exacte specificationem codicem scribere debes? Summa: debet esse uno gradu altiori ipso codice. Status et mores describere debet. Sit tam stricte quam negotium postulat. Si specificationem scribis quomodo ad negotium conficiendum, illud in pseudocode vel cum PlusCal scribere potes. Discere debes scribere specificationes in specificationibus formalibus. Hoc tibi necessarias artes dabit, quae te tam tacitis adiuvabunt. Quomodo formas specificas scribere discis? Cum programmata didicimus, libellos scripsimus et inde deprimimus. Idem hic: specificationem scribere debes, exemplar tessellatum reprehendo, errores fige. TLA+ non potest esse optima lingua pro specificatione formali, et alia lingua verisimilius melius erit pro certis necessitatibus tuis. Commodum TLA+ est ut mathematicos optime docet.
Quomodo ligare speciem et codicem? Ope commentaria quae notiones mathematicas coniungunt eorumque exsecutionem. Si cum graphis laboras, tum in ordine programma habebis nodorum vestitus et nexuum vestitus. Ideo accurate scribere debes quomodo grapha his structuris programmatis perficiatur.
Notandum est, quod nullus praedictorum valet de actu scripturae in codice. Cum codicem scribis, id est tertium gradum perficis, etiam debes cogitare et cogitare per rationem. Si subtask evadit complexus vel non manifestus, scribere debebis specificationem pro eo. Sed non de ipso codice hic loquor. Qualibet programmandi lingua, qualibet methodo uti potes, non est de illis. Item, nullus predictorum excludit necessitatem examinandi et debug codicem. Etsi exemplar abstractum recte scribitur, cimices possunt esse in exsequenda.
Specificationes scripturae gradus additi sunt in processu coding. Ob eam multi errores minore labore capi possunt - id ab experientia programmatum Amazonum novimus. Cum specificationibus, qualitas programmatum altior fit. Cur ergo toties caremus? Quia difficile est scribere. Scriptura autem difficilis est, quia ad hoc debes cogitare, et cogitatio quoque difficilis est. Facilius semper est quod sentias simulare. Hic potes analogiam trahere cum currendo, quo minus curris, eo tardius curris. Opus est tibi musculos instituendi et scripturam exerce. Usu eget.
Specificatio potest esse falsa. Posses alicubi errasse, vel requisita mutari possent, vel emendatio fieri posset. Quodlibet codicem quo quis usus mutandus est, specificatio tam citius aut serius non amplius congruit progressioni. Specimen, in hoc casu, novam speciem scribere debes et codicem omnino rescribere. Neminem id facit optime novimus. In usu codicem repeciamus et specificationem fortasse renovamus. Si hoc tenetur citius vel serius fieri, cur omnino specificationem scribimus? Uno modo, pro eo qui codicem tuum recensebit, omne verbum extra nominationem in auro valebit, et hic homo bene tu ipse erit. Saepe me graviter castigare non satis specificationem questus sum cum codicem meum emendo. Et plura specimina scribo quam codicem. Cum igitur codicem recenseas, nominatio semper renovanda est. Secundo, unaquaque recognitione, codice deterioratur, magis ac difficilius fit legere et conservare. Hoc entropy auctum est. Sed si a spectionem non incipias, omnis versus quem scribes recensendum erit, et codex obnixus erit et difficile ab initio legetur.
sicut dixit , nec consilio nec pugna parta est. et sciebat rem aut duos de proeliis. Opinio scripturae determinationes esse superfluum est. Aliquando hoc verum est, et negotium tam simplex est ut nihil per eam cogitare possit. Sed semper meminisse debes, quod cum tibi dictum est non scribere speciem, tibi dictum sit non cogitare. Et de illo omni tempore debes cogitare. Ratus per negotium non spondet te non errare. Ut novimus, nemo magicum invenit, et programmatio difficilis est. Sed si per problema non cogitas, spondetur errare.
Plus legere potes de TLA + et PlusCal in loco speciali, illuc ire potes e pagina mea . Ista omnia mihi, tibi gratias agimus ob animum tuum.
Nota quaeso hanc translationem esse. Cum commentarios scribes, memento auctorem illos non legisse. Si vere cum auctore colloqui vis, tunc in colloquio Hydra 2019 erit, quod die 11-12 mensis Iulii anno 2019 in St. Petersburg habebitur. Tesseras potest possideri .
Source: www.habr.com