summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Mon, 31 Jul 2017 14:03:47 +0200 | |

changeset 69878 | 9c7fe85cafd3 |

parent 69877 | 3a4da8caad49 |

child 69881 | 27fdaedc994e |

scores

--- 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