Semantics, Verification and Validation

Does it do what it is supposed to? Is that the right thing for it to do?

Computer programs can fail for lots of reasons. The can have bugs that mean they don’t do what they we intended to do. However, that thing they were supposed to do could be flawed. This is the difference between verification and validation.

Verification also depends on semantics: having mathematically defined meanings of programming languages. They provide the foundation for formal reasoning about whether programs are correct.

Find out more about how to prove both programs and algorithms are correct…

Why ‘Correct’ Computers Can Be So Wrong

A dark, brooding vending machine

Have you ever followed a recipe perfectly, only to find the cake tastes… well, a bit weird? You followed every rule, measured every ingredient, and checked every step. The recipe said you did it right. But your taste buds, and your grandma’s disappointed sigh, told you something was definitely wrong. In the world of computer science, we have this problem all the time. We call it the difference between verification and validation. Vasileios Klimis has been exploring the use of mathematical genies to help with validation. (Read on)

The Proof of Love

For Valentine’s day we created this card with a pseudocode love poem. But what does it mean? Is it a statement of love or not? Now that Valentines Day is gone and logic and rational thinking are starting to reassert themselves, here is a logical argument of what it means: an informal proof of love. (Read on)

Peter Landin: Elegance from Logic

A key idea behind programming language design is that a language should make it easy to write complex algorithms in simple and elegant ways. It turns out that logic is key to that. Through his work on programming language design, Peter Landin as much as anyone, promoted both elegance and the linked importance of logic in programming. …(read on)

The logic behind syntactic sugar

Computer Scientists talk about “Syntactic Sugar”. But in what way might a program be made sweet? It is all about how necessary a feature of a language is. The phrase was invented by Peter Landin. He realised it made it easier to define the meaning of languages in logic and made the definitions more elegant. …(read on)

Philippa Gardner bringing law and order to a wild west

The computing world is a wild west, with bugs in software the norm, and malicious people and hostile countries making use of them to attack people, companies and other nations. We can do better. Philippa Gardner has dedicated her working life to rectifying this by providing ways to verify software, so mathematically prove such trust-based properties hold of it. (read on)

Conjuring with logic: the remote control red-black mind-meld

We outline a magic trick and show how to prove it works. Magic tricks are just algorithms – they involve a magician following the steps of the trick precisely. But how can a magician be sure a trick will definitely work when they do it in front of an audience? Just like computer scientists who can prove their algorithms always work, a magician can use logic and deduction to be sure their tricks always work too. … (read on)

Complexity and Algorithms

Computer scientists invent algorithms then explore the properties of them, including proving mathematically that they work. However, just working is not enough. They must be efficient to. What are the bounds on what algorithms can even do at all? It is not of much practical use inventing an algorithm that will take longer then the age of the universe to give an answer, so understanding the maths of how efficient algorithms are – how complex they are really matters. And it leads to one of the most important but unsolved problems in all of Computer Science.(Read on)

Conjuring with Logic and Deduction

Find out how we can prove that magic tricks work just as we prove software works in out book on Conjuring with Computation… (Read on)

Subscribe to be notified whenever we publish a new post to the CS4FN blog.

This blog is funded by EPSRC on research agreement EP/W033615/1.

QMUL CS4FN EPSRC logos