Disabling throwing exceptions (e.g. in /include/iprt/cdefs.h) can be achieved using throw().
“extern C” prevents name-mangling.
VirtualBox CDefs.h
Reply
The Java Module System
Watch the JSR 277: Java Module System video from the Advanced Topics in Programming Languages Series
Upgrading From Fedora Linux 14 to 16
Today was the first time I upgraded a Fedora system (I use Ubuntu).
Coq Lessons
The difference between {x = y} + {x <> y} and x \/ y is whether the result is of type Prop or type Set.
Inductive or (A B:Prop) : Prop :=
| or_introl : A -> A \/ B
| or_intror : B -> A \/ B
The only feature of Section is to apply all the “Variable”s as implicit first arguments to everything listed in the particular section.
Searching for an element in a list is essentially an existsb operation.
Compare the following theorems:
Theorem C_eq_dec:
forall (x y:C), {x = y} + {x <> y}.
Proof.
intros x y.
decide equality.
apply id_eq_dec.
Qed.
Theorem C_eq_dec:
forall (x y:C), {x = y} + {x <> y}.
Proof.
intros x; case x as [|id_x]; intros y; case y as [|id_y]; eauto.
right; intros H; inversion H.
right; intros H; inversion H.
case (id_eq_dec id_x id_y) as [EQ|NEQ]; [ rewrite EQ; left | right ]; eauto.
intros H; eapply NEQ; inversion H; eauto.
Qed.
The first version uses the decide equality tactic. Note that the ML program can be obtained using “Extraction C_eq_dec.” C_eq_dec is also a function that can now be called. For example, it can appear in a match expression like:
match C_eq_dec c c’ with
| right _ => None
| left _ => Some (HeapObj c cfll)
end
where left and right constructors are explained in Specif (under Inductive sumbool …).
As for declaring “Heap” as a map, here is the syntax I finally got to work. Apparently the requires are important (using fully qualified names without them did not work).
Require Import Coq.FSets.FMapWeakList.
Require Import OrderedTypeEx.
Module MyModule (Heap:FMapInterface.S with Module E := Nat_as_OT).
Coq Syntax
I’m learning how to use the FMapInterface class of modules in Coq. A search for FMapInterface led me to A Machine Checked Model of Idempotent MGU Axioms For
Lists of Equational Constraints which had a link to its corresponding Coq script. Poking around in that script led me to the line:
Module Nat_as_MyOT <: UsualOrderedType := Nat_as_OT.
I looked up the meaning of the <: syntax. The reference manual explains that it “starts an interactive module satisfying each” subsequent module type. The ModuleSystemTutorial page also has more information on how modules are used.
Racket directory-exists? Handlers
Today I experimented with how to handle Racket’s directory-exists? exception thrown when the empty string is passed:
(define (isdir? dir)
(cond
[(with-handlers ([exn:fail:filesystem?
(λ (x) #f)]
[exn:fail?
(λ (x) #f)]
)
(directory-exists? dir))]
[1]))
(isdir? “”)
Breaking Software
I just got my copy of “How to Break Software” yesterday. I read through the first half today and already caught a couple of issues in the DrRacket IDE. Choose File -> Search in Files and then clear the directory name input and click OK. Some exception window shows up. Next, try setting the font size by dragging the slider in preferences all the way to the left. The program hangs instantly, and the erroneous setting is stored for the next startup. The only way to recover is to manually edit the config file in %appdata%/Racket to save the day.
EigenCFA
We discussed the paper EigenCFA: Accelerating Flow Analysis with GPUs in CS630. 0-CFA is one of the simplest CFA algorithms and yet is still “nearly” cubic hence the author’s efforts…
Longest Common Nonsequential Subsequence
If we need the longest common sub-sequence of two strings but with the caveat that we are only interested in having all the right letters & frequencies, and not their orders, then dynamic programming isn’t really necessary. This boils down to the problem of finding the largest common subset of the two sets of letters in the two strings.
The Fifteen Puzzle
I remember playing the fifteen-puzzle game on our first computer – an 80486 running Windows 3.1. It was a variation that used images instead of numbers, but I still remember how intriguing it was at that age. Well, today is the first time I’ve figured out it’s official name, thanks to some brainstorming with the folks in the lab (& Google, obviously).