--- a/Exercises/hwsubm/OR/Erhard_Julian_ga48kog@mytum.de_655/quadtrees.thy Mon Jul 31 09:34:31 2017 +0200
+++ b/Exercises/hwsubm/OR/Erhard_Julian_ga48kog@mytum.de_655/quadtrees.thy Mon Jul 31 14:03:47 2017 +0200
@@ -1,4 +1,11 @@
-(*\<Rightarrow> Tobias*)
+(** Score: 13/15
+
+Reasonable formalization of quad trees. But you have not proved anything about delete. And
+what you proved about insert is not quite enough. Moreover, you should have
+commented it better. One has to guess what are the programmers interface
+functions, what are local functions, and what are specification functions.
+*)
+
theory quadtrees
imports Complex_Main
begin
--- a/Exercises/hwsubm/OR/Hellauer_Fabian_f.hellauer@tum.de_656/FDS_hw.thy Mon Jul 31 09:34:31 2017 +0200
+++ b/Exercises/hwsubm/OR/Hellauer_Fabian_f.hellauer@tum.de_656/FDS_hw.thy Mon Jul 31 14:03:47 2017 +0200
@@ -1,4 +1,11 @@
-(*\<Rightarrow> Tobias*)
+(** Score: 9/15
+
+
+Mainly extensions of existing work, with only a few definitions and proofs of
+your own. Moreover the originality factor is not that high.
+
+*)
+
theory FDS_hw
imports
Complex_Main
--- a/Exercises/hwsubm/OR/Hutzler_Matthias_ga95luy@mytum.de_638/digits_arithmetic.thy Mon Jul 31 09:34:31 2017 +0200
+++ b/Exercises/hwsubm/OR/Hutzler_Matthias_ga95luy@mytum.de_638/digits_arithmetic.thy Mon Jul 31 14:03:47 2017 +0200
@@ -1,4 +1,9 @@
-(*\<Rightarrow> Tobias*)
+(** Score: 20/15
+
+Nice and original work on floating point numbers.
+
+*)
+
(* Author: Matthias Hutzler
Some arbitrary precision arithmetic with lists of binary digits.
--- a/Exercises/hwsubm/OR/Oganyan_Levon_levon.oganyan@tum.de_647/hmw11.thy Mon Jul 31 09:34:31 2017 +0200
+++ b/Exercises/hwsubm/OR/Oganyan_Levon_levon.oganyan@tum.de_647/hmw11.thy Mon Jul 31 14:03:47 2017 +0200
@@ -1,4 +1,13 @@
-(*\<Rightarrow> Tobias*)
+(** Score: 12/15
+
+Decent formalization. But you did not formulate and prove precise correctness conditions
+for your functions. For checkPos you say so yourself. The reason is that you
+were too fixated on type real, but your trees represent discrete points in
+space. You should have defined an abstraction function that maps an OctTree
+into a set of points with nat (or int) coordinates. Then you could have
+specified your functions intersect, merge and checkPos quite easily.
+
+*)
theory hmw11
imports Complex_Main
begin
--- a/Exercises/hwsubm/OR/Wauligmann_Martin_martin.wauligmann@tum.de_642/Quadtree.thy Mon Jul 31 09:34:31 2017 +0200
+++ b/Exercises/hwsubm/OR/Wauligmann_Martin_martin.wauligmann@tum.de_642/Quadtree.thy Mon Jul 31 14:03:47 2017 +0200
@@ -1,4 +1,13 @@
-(*\<Rightarrow> Tobias*)
+(** Score: 12/15
+
+Reasonable formalization of quad trees. But you did not formulate and prove precise
+correctness conditions for your functions. You may have tried to do so via the
+count_pixel function but that is insufficient. You should have defined an
+abstraction function that maps a quad tree to a set of (nat,nat) points. Then
+you could have specified the desired behaviour of union and intersection
+quite easily.
+
+*)
theory Quadtree
imports Main
begin