Posts

Showing posts from 2014

A tiny proof checker in Prolog

The Prolog code for this post is available on GitHub . I am crazy enough to teach Hoare logic (axiomatic semantics) in the first course for our CS students. For instance, consider the following program (in some simple imperative language), which is supposed to compute quotient q and remainder r according to Euclidian division for operands  x and y : q = 0; r = x; while (r >= y) { r = r - y; q = q + 1; } Given natural numbers x and y , the postcondition of the program is this: x == q*y + r && q >= 0 && r>=0 && r < y The precondition is this is: x >= 0 && y > 0 We are supposed to prove the "triple" consisting of precondition, program, and postcondition. Let's face it, verification according to Hoare logic is not easily understood by beginners. Many of my students aren't mathematically / logically fit, when they enter the curriculum. So it is a pain in the neck for them to listen and for

My Gear Fit Wish List

For like 10 days I own and use a  Samsung Gear Fit . I love it. I don't agree with this  negative review . However, I hope Samsung improves the software in a timely manner. Here are some proposals, I should edit this blog post, as I see fit. Bug report : Cycling exercise stops recording because of "no movements" This happens after 10mins of recording. I think this happens because it uses a sanity check that may be right for running exercises, but there is no arm/hand movements, if you are cycling in a proper way. Within some time window, I can cancel the stop message to make it continue measuring. Anyway, this is highly annoying, as I need to hit a small on-display button while cycling. I don't see how one could not have caught this by basic field testing. [Added on 19 May 2014] Feature request : Usable wake-up gesture needed Currently, we have the choice between pushing the small hardware button on the Gear Fit to wake it up or relying on movement-bas