Showing posts with label Logic. Show all posts
Showing posts with label Logic. Show all posts

Monday, 11 May 2015

Wizards and Warriors

What Could Possibly Go Wrong?
Players, such as wizards and warriors, have weapons; such as staffs and swords.
So innocuously begins Eric Lippert's latest forage into object-oriented design. Like all of his best work, this adventure soon takes us into various intuitive dead ends and surprising ambush back-alleys. You will nod sagely as he overcomes each successive objection, excises each fly from the ointment, with a new design principle or approach; THEN CURSE as your newest paradigm rears up and bites you in the assets. Finally, you will marvel at the astonishing and enlightened conclusion of it all, by which time you will have become a better human being in every sense that matters (to an object-oriented software designer).

Enjoy it here:
Part One
Part Two
Part Three
Part Four
Part Five
Note: the "DSLs" that emerge toward the end of Part Five are of course Domain Specific Languages.

Wednesday, 5 December 2012

SA1503: CurlyBracketsMustNotBeOmitted (Part 1)

Parenthetical Remarks

StyleCop rule SA1503 is designed to complain whenever
The opening and closing curly brackets for a C# statement have been omitted.
What does this mean, and is it a good rule?

Syntactic Structures

In C#, the bodies (or consequents) of certain flow control and looping constructs, such as if, while, and for statements, can syntactically be any single statement. For example, the underlined statements below are all single-statement bodies:
if (x == 1)
  y = 2;
else
  z = 3;

while (x < 10)
  x++;

for (var i = 0; i < 10; i++)
  x *= i;
Obviously there are times when you want the body of your construct to contain, rather than a single atomic statement, a sequence of two or more such statements. This is accommodated by the use a special type of single statement called a block, comprising just the required sequence of statements enclosed in curly braces, as shown below. Note that the entire contents of the curly braces, including the braces themselves, still comprise a single statement - which just happens to be of the block type:
if (x == 1)
{
  y = 2;
  z = 3;
}
These flow control and looping constructs can be nested within one another. A simple example of such nesting is this:
if (A())
  if (B())
    C();
  else
    D();
Since the rule in C# is that an else clause gets associated with the nearest available if statement, the else in this example has been indented to line up correctly with the second if statement, to which it properly belongs.

Problem?

Some people point out that the indentation can be applied incorrectly, and that the resultant statement
if (A())
  if (B())
    C();
else
  D();
can be ambiguous. Of course it's not ambiguous; after all, the compiler has absolutely no problem in applying the correct rules of precedence in a case like this, and coming up with the one correct result. However, it is true to say the above example is confusing, since it looks as though the else clause refers back to the first if statement rather than matching the second. The obvious remedy is to correct the indentation - and in fact to enforce consistent and correct indentation in future, so that such confusion cannot occur.

A Bad Fix

Sadly, those same people who insist on allowing badly formed indentation to pollute their code, often compound their error by suggesting a rather odd way of fixing it. Simply disallow any statement type except a block in these contexts! The result is a proliferation of brackets:
if (A())
{
  if (B())
  {
    C();
  }
  else
  {
    D();
  }
}
Although much harder to read, this version does at least have the virtue that its intention is quite clear. However, that clarity has not come about from the addition of braces. No, the alignment of the braces merely served to highlight the indentation error which was causing the confusion, and which incidentally has also been corrected in this latest version. Correct the indentation and we remove the confusion, braces or none. If anything, the braces are making it more difficult to follow the structure of nested statements like these, by making them twice as tall as they need be, and physically separating the components that you're trying to line up visually.

Another Example

In the above referenced documentation of rule SA1503, the following example is given:
if (true)
  this.value = 2;      
  return this.value;

Glancing at this code, it appears as if both the assignment statement and the return statement are children of the if-statement. In fact, this is not true. Only the assignment statement is a child of the if-statement, and the return statement will always execute regardless of the outcome of the if-statement.
Okay, so far I'm agreeing with you. But sadly we soon descend into nonsense:
StyleCop always requires the opening and closing curly brackets to be present, to prevent these kinds of errors:

if (true)
{
  this.value = 2;      
  return this.value;
}
Yeah, no. Now this so-called example lacks any credibility. Look, if that first fragment compiles, the one without the braces, then it must be sitting at the very end of its enclosing method - because it ends with an unconditional return, anything after which is unreachable code. Which of course you're already detecting, and in fact treating as an error, right? Right, so it's the last thing in the method. But this means that the second version can't compile at all, since there needs to be another unconditional return statement after it; the compiler will be justly livid about its absence (not all paths return a value, nag nag nag...).

Preliminary Conclusion

When I started looking into this issue, I was inclined to accept switching on rule SA1503. Anecdotal evidence seemed to support the idea that it could prevent bugs. And then, for me at least, there was this clincher: even Eric Lippert appeared to be suggesting that compulsory braces represented a solution to the classic dangling else problem, and one which he wished had been applied to C# from day one!

Then I realised that SA1503 wanted to do much more than just enforce braces in an if statement where an else clause was present. It wanted braces everywhere! That was when I began to pay closer attention to the arguments being offered, both for and against the measure.

The faulty examples above are typical of much I've encountered in researching what now appears to me a particularly misguided and ineffectual StyleCop rule. In seeking to mitigate against bad code layout by making wholesale changes to its syntactic structure, we not only miss our target entirely, but find ourselves instead lowering the code quality and readability. SA1503 therefore seems a bad rule from this perspective.

Next time: quick edits & legacy code.

Monday, 30 April 2012

My Work in Print: 1987

Previously: 1985

DISZ80 - a Z80 Disassembler

Delighted today, to receive a comment from Geoff Wearmouth on that previous Personal Computer World: Sub Set article. Geoff it was, who first typed my 1094-byte Z80 disassembler DISZ80 into a Sinclair Spectrum some quarter century ago. His site http://www.wearmouth.demon.co.uk/ gathers Sinclair ZX Spectrum ROMs, as well as emulation tools for the related ZX80, ZX81, and the eternally awe-inducing Jupiter Cantab Ace.

Geoff's own Spectrum Globeplotter, featured in The Register Hardware's Basic Instinct last week, and itself more than a quarter century old, proves us to be PCW stablemates. Whilst presented as a BASIC listing, this spinning-sphere-transpoising, sinusoidal-Mercator-projecting screen plotter actually employs untold amounts of custom crafted machine code.

Some ten years ago, Geoff made appeals in comp.sys.sinclair for any further information about PCW back issues. And just today, Stephen Parry-Thomas of http://jupiter-ace.co.uk/ has replied, with full scans of Sub Set from February-May 1987. At last, the extensive line comments can be restored to my crusty old utility!

February 1987

Click to big. In "Z80 Radix Conversion" David Barrow starts off with CONVHL, which is used at various points within the main disassembler to convert 16-bit integers to various bases (binary, octal, decimal, hex) for readable output. He remarks upon the "quite ingenious" optimised method used to convert raw digits to ASCII.

I remember being quite happy with the way David had split out the various modular components of the program. Publishing these in multiple datasheets over several months resulted in a steady stream of payments, giving a pleasant illusion of gainfully paid employment!

March 1987

March saw the publication of routine XTRACT, designed to read and print strings from a table. As David correctly notes, this too is pathologically storage space optimised, for both code and data table size.

April 1987

The I/O fest continued in April with a set of five connected utilities dealing with the output of hex data and addresses. This is the point at which David, having correctly diagnosed my space optimisation compulsion, shows where I could have saved one program byte, two stack bytes and 14 clock cycles. Though 25 years later I've still to validate the assertion, respect for David's manifest expertise compels me to believe it, albeit truculently.

May 1987

The May edition was given over to just the two remaining big routines, spread across five new datasheets / appendices, and completing the 1094-byte Z80 disassembler.

So, once again: hooge thanks to the guys, Geoff Wearmouth and Stephen Parry-Thomas, who got these page scans to me - I do hope you'll both understand and forgive the indecent haste with which I've posted them here.

Try It Out!

Finally, Geoff's just been in touch again to tell me that DISZ80 is actually live online, and has been for years, embedded in his ZX Spectrum Emulator. How cool is that? Click here to run it. I just tried it out using Internet Explorer 8, 64-bit (!) version. Click the "screen" then press Enter for instructions. The Disassembler itself can be disassembled (!!) by typing the address $5100 then pressing Enter. The code you see starting at that address is actually the DISZ80 entry point, as illustrated in the first of the May 1987 pages above. Mind = Blown!

Friday, 13 April 2012

Tri-State Logic in C#

First, a Story About Trees

Certain friends and colleagues, asking me about the origin of my "Stanislaw" Facebook persona, have already been introduced to the shady night dweller "Stanislaw the Philosopher". Found in and around 1980 sweating over some maths and engineering textbooks in the wee small hours, listening to Mike McLean Through the Night on Radio Clyde, and occasionally sending in record links in the form of unbearably awful puns. Like this:
The king's gardener feared for his life. Long and hard he had toiled in the royal grounds, trying desperately to make the castle's fir trees thrive in the dry, dusty and too-barren earth. Nothing would work to save them. And now that his life was forfeit, he had begun to see ghosts during his nightly rounds. One of these came up to him, holding forth a small cloth pouch, and saying "These are the droppings of the kestrel hawk. Lime for this climate, bone for these flora. You must feed it to their roots, one and all. For either you and they shall die, or else neither."

The gardener did as he was bid. Three nights later, walking through the grounds in the dark of an otherwise still night, he now sensed those trees rising up before and around him, moment by moment blocking off a little more of the violet horizon. Was this truly and solely an imagination? Then too, he began hearing something wholly unaccustomed and chilling on the air, what was that sound? The raising of a distant breeze, the creaking of old bones and branches, the arrival of some new monster unseen?

Or kestrel manure firs in the dark?



On another occasion, Stanislaw the Philosopher posed a riddle from Raymond Smullyan's book of logical puzzles, What Is The Name Of This Book? The hardback book itself was sent to the radio station as a prize. Stanislaw then sent in the correct answer under the guise of his good friend Tom, who was subsequently baffled to receive such a book, from a radio station he never listened to, as a prize in a competition he'd never heard of.

But Seriously...

This whole confession is prompted by Eric Lippert's blog Fabulous Adventures in Coding, and in particular by today's entry, null is not false, part two. Eric starts off by using Dr Smullyan's deductive logic puzzle books to introduce the concept of multi-valued logic systems, including the nullable boolean. This 3-state scheme has the possible values: true, false, and null.

The rules of null are quite straightforward and obvious, if you think of replacing it everywhere with "unknown". So for example in arithmetic, we would have
X + null = null,
which translates as the self-evident "Anything plus unknown, equals unknown." Now in our 3-term logic,
false AND Y = false,
since whatever the second term might represent (including null), the first false makes the expression false. But this also implies that
X AND false = false,
which can be a problem for computer languages featuring short-circuit boolean evaluation. Eric considers the cases of the C# operators && and ||, which are specified as strictly short-circuiting operators, and asks the question, how should we evaluate
X && Y
when X is null? The truth table gives unambiguous answers: false if Y is false, otherwise null. But to obtain that answer we had to violate the specification that Y is only evaluated when X is true. Eric closes by saying "...either we sometimes evaluate Y when we shouldn't, or we sometimes return a value that does not match the value that X&Y would have produced. The way out of this dilemma is to cut the feature entirely."

So, the operators && and || are not "lifted to nullable". That seems a shame! I'd have preferred the alternative way out of that dilemma, where we allow nullable overrides of these operators, and simply replace the pair of statements
In the expression X && Y we evaluate Y if and only if X is true
In the expression X || Y we evaluate Y if and only if X is false
with
In the expression X && Y we evaluate Y if and only if X isn't false
In the expression X || Y we evaluate Y if and only if X isn't true

Saturday, 5 November 2011

My Work in Print: 1985

I've previously written about the very competitive crafting of optimum machine code programs for Personal Computer World magazine's 1980s Sub Set series, here and there. In 1985, the incumbent series editor David Barrow convinced Century Communications to publish two books of the best submissions. According to the descriptions on their publication history pages, these books were "Edited and produced working directly from the author's word-processor by NWL Editorial Services, Rushley, High Ham, Somerset" - a huge novelty in the publishing world at the time. Book geeks: note the cool adjacent ISBNs!

Best of PCW Assembler Routines for the Z80

Although the first IBM PC with its 8-bit Intel 8088 chip had already been available for about four years, still most business software was based on the CP/M operating system, and the more powerful, backward compatible Zilog Z80. Joined to legion Sinclair hobbyists, these users constituted quite an army. Here is the index of my contributions to the Z80 edition:
  • ECAL - Calculate error correction byte; pp. 70-71.
  • EFIX - Validate data with error correction byte; pp. 71-72.
  • NEWPC - Anticipate PC contents after next instruction; pp. 78-82.
  • RDM32 - 32-bit pseudo-random number generator; pp. 147-149.
  • SQR31 - Square root of 32-bit signed (positive) value; pp. 169-170.
  • SQR32 - Square root of 32-bit unsigned (absolute) value; pp. 169-170.
  • CURT16 - Cube Root of a 16-bit unsigned integer value; pp. 170-174.
  • CURT32 - Cube Root of a 32-bit unsigned integer value; pp. 174-176.
  • SDIV4 - 4-byte signed integer division; pp. 183-185.
Barrow, David (editor)
Best of Personal Computer World Assembler Routines for the Z-80
Century Communications Ltd
1985
ISBN 0 7126 0506 1

Best of PCW Assembler Routines for the 6502

While businessmen cycled their Z80s, many hobbyists with an aversion to dead-flesh rubber keyboards were devouring Commodore VIC-20s and 64s, and Acorn's BBC Micro. All of these used the MOS Technology 6502 processor. Here is the index of my contributions to the 6502 edition:
  • RINXY - Register Indirect addressing mode emulator; pp. 20-22.
  • ECAL - Calculate error correction byte; pp. 88-90.
  • EFIX - Validate data with error correction byte; pp. 90-91.
  • SQR15 - Square root of 16-bit signed (positive) value; pp. 125-127.
  • SQR16 - Square root of 16-bit unsigned (absolute) value; pp. 125-127.
  • SQR31 - Square root of 32-bit signed (positive) value; pp. 127-129.
  • SQR32 - Square root of 32-bit unsigned (absolute) value; pp. 127-129.
  • CURT16 - Cube Root of a 16-bit unsigned integer value; pp. 129-134.
  • CURT32 - Cube Root of a 32-bit unsigned integer value; pp. 134-137.
Barrow, David (editor)
Best of Personal Computer World Assembler Routines for the 6502
Century Communications Ltd
1985
ISBN 0 7126 0507 X

A Disassembler in ~1KB


Colleague C keeps reminding me that The SUBSET editor David Barrow was able to trim only one byte from John Kerr's compact code. What the hell is he talking about? The quote comes from this ZX Spectrum Utility, whose author explains: The stated aim was to write a Z80 disassembly routine in as short a space as possible and, at just over 1K (1090 bytes), it is a rather incredible program.

Unfortunately my DISZ80 routine was submitted too late - by about two years - for inclusion in the book, and I no longer have the magazine that it appeared in. At the risk of sounding a bit JR Hartley, if anyone out there has that 1987 issue, it would be good to be able to restore the line comments to the utility. I work in self-documenting, high level languages now, eschewing comments almost universally. But part of the strict Sub Set documentation standard insisted that every single machine code instruction got fully commented. Oh, and it would also be nice to see exactly where Dave Barrow's one-byte optimization appeared!

[Update 30 April 2012: This has now been done, many thanks to my new best friends Geoff Wearmouth and Stephen Parry-Thomas! See comments below, and also My Work in Print: 1987]

Cube Root Algorithm

I derived the method of cube root extraction used in both books, by applying a kind of induction by analogy to the existing square root algorithm. Dave thought my description of the process sufficiently interesting to publish it. Click for readability:



Next time: 1987

Saturday, 8 October 2011

Quantum Computing for the Determined

Moving Pictures

Nobody seems willing to predict when quantum computing will take off. Some are even beginning to question whether it will ever do so. Meanwhile, optimists patiently await that crucial breakthrough, the discovery of the perfect physical realisation of the qubit. There's no shortage of candidates. The Nitrogen Vacancy (NV) centre in diamond is one. NVs are the crystal lattice imperfections in pink diamonds that give them their hue. Then again, a lot of progress has recently been made involving trapped ion systems.

The optimists wait - impatiently, on second thoughts! - for one of these, or for some other exotic virtual particle inhabiting some material (or as yet unknown metamaterial), that will finally and abruptly realise the qubit as coherent, entangled and scalable.

As they wait, they polish their grasp of linear algebra, matrices, the various fundamental and second-order quantum "gates" that have been conceived, and the circuits made possible by these. Rehearse the limitations imposed by their fragility and inscrutability. Marvel at the astonishing algorithms that have been developed in qubit theory, while worrying about their scant number and opaque discoverability.

Almost to a man or woman, they have found and honed their new algebraic skills using The Book: Quantum Computation and Quantum Information, by Michael A. Nielsen (University of Queensland) and Isaac L. Chuang (IBM / Stanford University). Or Mike and Ike, as this revered tome is universally known. A literally pioneering work, it was the first of its kind, and is still today the standard to which all else is inevitably compared (my earlier review is here). In fact it's the most highly quoted physics publication of the last 25 years, and one of the ten most highly quoted physics books of all time (source: Google Scholar, December 2007).

In support of its tenth anniversary edition, Professor Nielsen has released a set of 22 short video lectures on his blog. They're a great introduction to the subject. However, he has stopped just short of completing the course, due to intervening work commitments. He has promised to complete it if there's enough interest in the videos produced so far. Here's the first one:



You know what you must do!

Next time: Single Qubit Gates.

Friday, 9 September 2011

Algebra

Don't you just hate those Microsoft developers?*

You've just started replacing that fusty old, string-based SQL Builder with a modern, class-based model, featuring fully composable queries, query clauses, and expressions, all the way down to basic arithmetic. Suddenly, they bring out LINQ.

Some time later, recognising the monadic algebra behind the new pattern-based query comprehension keywords, you decide to harness it to implement the continuation monad, which will allow you to write asynchronous code in a purely synchronous paradigm. Suddenly, they announce async/await.

No matter how good, how revolutionary your design, the fact remains that you just can't beat a good keyword. There's simply no better or more powerful implementation, nothing tidier than a well conceived and designed primary language feature. This observation highlights the need to know thoroughly, completely and perfectly, the nature of the feature under implementation.

Unless your main business is writing compilers, your greatest enemy is the client specification, perhaps represented by the design engineer, stating non-goals like there is no requirement to compare or subtract two fields. Because you know that there will be. And when that requirement is finally unearthed, you will already have been forced down the Agile pipe, and have implemented a horribly hobbled subset of the operations that would have been required to express properly a well-formed algebra - of queries, or asynchronous tasks, or whatever.

The sad truth is that many of us lack the basic mathematical skills to appreciate the seachange wrought on your design by a proper, complete, closed and proven algebra. And while the scope for such effort and expenditure by application developers continues to shrink, and a good job too, with the increasing power and usability of production compilers and other tools; still it is imperative to be ready to identify such situations when they do occur, and to be prepared to design the solution along veins of sound, algebraic principles.

Vindication

Eric Lippert's latest blog article is a beautiful exercise in such pure, abstract, algebraic thinking, and brilliantly displays its payoff. He asks, what in C# is a type? The naive answers most of us would propose, these have all by now been discounted with the aid of counterexamples, in the predecessor article. A type is not a name with a set of values. Neither can it be defined as a set of assignment rules. Still less is a type some kind of predicate for determining which among an infinite set of values belong to it. Eric demonstrates the strictly formal application of mathematical logic at work in his conception, when he actually makes essential use of Russell's Paradox in proving the inadequacy of these attempts!

A type, in the mind of compiler writer Eric, is nothing more than an abstract mathematical entity obeying certain algebraic rules. He follows this definition with a good analogy based on Giuseppe Peano's axiomatic definition of natural number. Turning back to his equally axiomatic type definition, he then shows how its axioms can be used to construct compile-time proofs of runtime type safety (ignoring temporarily wrinkles like the cast operator, or unsafe array covariance).

But perhaps the best illustration of the power of the abstract analytical approach is seen when he dips into Gödel's undecidability results, and identifies areas where such proofs cannot be constructed reliably. The lesson here is that still, the formal analysis rigorously controls the progress toward a compiler solution; this time accurately and unambiguously delineating the "holes in the road" where practical workarounds must be applied, or where - in measurably unrealistic, and perfectly predictable situations - a compiler failure can be tolerated.

Expression too complex to analyse.

Pic: Giuseppe Peano, from Wikipedia. Not actually a Microsoft dev.
*I just love those Microsoft developers!

Friday, 20 May 2011

Is Jonathan Fargher Entirely Trustworthy?

Sony's Apology Package

Haven't had much to say about Sony's recent security troubles. Well, it's hard to travel anywhere on the news websites and blogs, without crashing into Floydian walls of opinion about the corporation and its permanently besieged Playstation Network. Even on the subject of this post, namely the "apology package", there are countless deafening choruses of "too little", "too late", "also, I want an Xbox", and related flamewars without end.

However

Jonathan Fargher, senior PR manager for Sony Computer Entertainment Europe (SCEE), has crossed a line with me. And I'm sure, with every other gamer with a gramme of technically literacy. If I may quote just two lines of his, from say the BBC's report:
  1. Clearly there's going to be a minority of people out there who have some of those games.
  2. We certainly believe [...] the choice of games that we're offering [...] is good value.
Of course I have to be careful what I say now, mindful of my country's draconian, and quite literally, unspeakably insane 17th century libel laws. But given these two statements, it is quite easy to prove with rigor, using little more than the rules of the predicate calculus, that Jonathan Fargher is either deranged, or a liar.

The proof doesn't depend on the truth or falsity of the individual statements themselves; given certain platitudes, it's as certain as any proof in logic, more so than any in the rest of mathematics. It is true regardless of whether or not some people already have some or all of these games; whether those people form a minority, or a majority; whether the choice of games is good value or a ripoff; and whether or not Jonathan Fargher believes some, any, all or none of the above. No single given factoid convicts. Rather, Jonathan Fargher's problem is that there's no consistent assignment of truth values to the various parts of his statements, that avoids the incriminating conclusion.

Reductio Ad Absurdum

We proceed by assuming the truth of everything Jonathan Fargher claims in those two statements above. From this we derive a contradiction. Finally we conclude that either Jonathan Fargher believes this contradiction, in which case he is arguably deranged; or alternatively, he doesn't actually believe (one or more of) his own claims. In that case, inescapably, he's a liar.

So, working from the back to the front: the second thing Jonathan Fargher believes is that the choice of games is "good value". How can we express this in less subjective terms? Let's take a look at that choice.

PS3 TitleRelease Date
Dead NationDec 2010
InfamousMay 2009
Little Big PlanetOct 2008
Ratchet and Clank: Quest for BootyAug 2008
Wipeout HD/FuryDec 2009

Apart from the PSN exclusive zombie shooter Dead Nation, and the Fury addition to warhorse Wipeout HD, everything here is two or more years old.

PSP TitleRelease Date
Killzone LiberationNov 2006
Little Big Planet PSPNov 2009
ModNation PSPMay 2010
Pursuit ForceNov 2005

Wow. I'd forgotten there even was a PSP console in 2005.

Yet regardless of the considerable age and the low current prices (below £10) of many of these titles, and notwithstanding the fact that you get to pick only two games from either list, none of this allows us to deny Jonathan Fargher's claim of "good value". Why? Because here, they're free. Any attempt to compute the value-for-money of a given selection results in a division by zero error.

That can't be right. Are we now agreeing with Jonathan Fargher, and going fargher still, to say that the selection represents infinite value? No. Clearly the concept of value-for-money is inapplicable to truly free offers. A better gauge is the popularity of the selections. The more popular the game, the higher its value as a free offering. But here we begin to see the seeds of the contradiction that we seek. In a given console community, popular games are by definition those most likely to be owned already. And to such an existing owner, a free download of such a game obviously has a very low value indeed.

Summing Up

From Jonathan Fargher's Second Law, we are being offered a "good value" selection of games, in other words, a set containing at least some popular games. By definition, such games are already owned by a majority of a given console community. That contradicts Jonathan Fargher's First Law, that no more than "a minority of people" will already have any of those games.

Quod erat demonstrandum.