SPARK Ada Examples from Lectures