SERG-Delft / jpacman-framework

Pacman-inspired game, for teaching testing purposes.
123 stars 254 forks source link

Adopt Checker Framework #101

Closed avandeursen closed 7 years ago

avandeursen commented 7 years ago

This branch is the result of applying null checks as offered through the Checker Framework to JPacman.

The checker framework's default assumption is that classes are non-nullable, so I added a couple of Nullable annotations where needed.

I also made some assumptions explicit through run time assertions (with the assert keyword), which the checkerframework then uses in its static analysis.

I suppressed all initialization warnings in the test classes (the checkerframework does not recognize JUnit (5) setup methods) -- and I could not find a way to disable null checking all test suites all together.

I made the getSquare method non-null, adding an explicit checker method for testing nullity which is then a precondition for getSquare.

Invariant methods invoked in the constructor lead to initialization problems from the checkerframework, which I eventually decided to suppress.

Potentially incorrectly unhandled null values occurred in the AI for determining next moves of ghosts, and in the handling of a resource in case of a reading failure.

This is a bit of a big bang pull request, since it is not so obvious how to enable null checking on just a few classes only.

After the null checks are integrated, we could consider adopting other checkerframework checks.

An open question is how this relates to Java 8 Optionals.

Insisting that students use the checkerframework in their own solutions is a decision that is separate from merging the pull request. The checkerframework does some deep analysis and requires thorough understanding of how Java works.

LiamClark commented 7 years ago

Did we figure out how to disable the codacy-bot yet?

LiamClark commented 7 years ago

A very subjective and opinionated summary:

Showing and making the students think about null-safety is a great idea! I have some experience with Kotlin and Swift that do this by default in their type systems and it works great!

This topic also highly ties in with mutability, hopefully i'll be clear enough here why. Consider we have a class containing one final field:

public class Foo {
      final Integer foo;
}

If we were to initialize the foo field with null what do we really get? A value that's guaranteed to always be null, which is rather useless. So for an immutable field (almost by design) it should never be null anyways.

This then brings us in to the second category mutable fields. These could start their life of as null and could become non-null later on. So there are 4 possible combinations for fields

  1. Immutable and NonNull (awesome!)
  2. Immutable and Nullable (useless?)
  3. Mutable and Non Null (okay)
  4. Mutable and Nullable (A nightmare)

Guiding students to 1. or 3. would be very nice.

Now we are here presented with two tools to showcase and solve this problem.

  1. The checker framework.
  2. Optional.

Regardless of which one might be better or work better I would like to highlight two things, Firstly what are we teaching the students with either approach. The checker framework will show the students some (In my opinion magic-y) annotations that annotate their source code to check for null-ability. Optionals show a gentle introduction to a mechanism that in this case solves null-ability, but can also be applied to other situations think Futures, Streams, Rx Observables or even distributed computing using apache Flink!

Optionals are also used in multiple languages for example Scala, Rust even c++17 use them as library types. The two others I mentioned earlier Swift and Kotlin even encode them in their language.

Secondly the first years students ability to pick this up. They are usually pretty familiar with Annotations due to JUnit and maybe some other libraries. Optionals in contrast are a little weirder concept. @TimvdLippe you have experience introducing second year students to them in the Concepts of programming languages course they struggled with it right?

Some of the code in Jpacman handles these concepts quite awkwardly and could definitely be improved.

So a concluding statement:

I don't disagree with introducing the checker framework and I can see valid reasons for doing so. It would however not be my preferred approach, but the optional approach might be too much load for the students. Regardless of the choice jpacman could indeed be improved in this aspect.

@avandeursen I would like to hear what you think!

TimvdLippe commented 7 years ago

@TimvdLippe you have experience introducing second year students to them in the Concepts of programming languages course they struggled with it right?

To my knowledge, Optional is not one of the concepts they were struggling, but can't say for certain.

foresterre commented 7 years ago

Did we figure out how to disable the codacy-bot yet?

@LiamClark I'm not sure whether you are still trying to figure out how to disable the codacy-bot (the comments), but in case you do: https://github.com/codacy-bot/how-to-unsubscribe

The explanation given:

I assume (hope) that this will also work for organisations (you can block github users through the Settings->Blocked users page of the organisation):

avandeursen commented 7 years ago

Thanks @foresterre: I lifted the block to the organizational level, let's see if this helps.

avandeursen commented 7 years ago

@LiamClark: Thanks for the Optional observations.

I like the declarative nature of the Nullable annotations, and find them a little more intuitive than the Optional types.

See also @mernst's comments: http://homes.cs.washington.edu/~mernst/advice/nothing-is-better-than-optional.html