Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Marking some fields in the returned object of a method NonNull and others Nullable? #3296

Closed
fzyzcjy opened this issue May 8, 2020 · 8 comments

Comments

@fzyzcjy
Copy link

fzyzcjy commented May 8, 2020

Hi! Thanks for the interesting library! A very simple question: I have a class (actually, a model, if you are interested) like -

class Article {
    int id;
    String text;
    int authorId;
    Date createAt;
}

And I have a class returning it:

interface ArticleRepository {
    Article getFullArticle(); /* return the Article with ALL fields being non-null */ 
    Article getBriefArticle(); /* return the Article with only `id` and `text` fields being non-null */ 
}

Question: How can I annotate that properly?

Thanks very much!

@mernst
Copy link
Member

mernst commented May 8, 2020

This is a good question.

The solution to your problem is qualifier polymorphism over classes.

Currently, the Checker Framework supports Java generics, and also qualifier polymorphims over methods.

Pull request #2883 implements qualifier polymorphims for classes. We are hoping to complete that feature soon -- in the next release or two -- but this depends on how much time everyone has to work on it.

@fzyzcjy
Copy link
Author

fzyzcjy commented May 9, 2020

Thanks very much! Hoping to see that!

@wmdietl
Copy link
Member

wmdietl commented May 10, 2020

The limited form of class qualifier parameters in #2883 will not help in this situation - and it won't help with the Nullness Checker in general. The main qualifier of a type is reused for the qualifier parameter - but if the main qualifier is @Nullable one won't be able to access the field regardless.

In the Article example, you could try making the fields @Nullable and then having a method like this:

    @EnsuresNonNullIf(result=true, expression="createAt")
    boolean isFullArticle() ...

We currently don't have a mechanism to specify as post-condition of getFullArticle(); that the resulting Article will satisfy isFullArticle.

@fzyzcjy
Copy link
Author

fzyzcjy commented May 12, 2020

Thanks very much!

@mernst
Copy link
Member

mernst commented May 12, 2020

The @Unused annotation might already solve your problem. It doesn't make a field nullable, but makes the field inaccessible, which is usually what you want. You would need to create a pair of new annotations @FullArticle and @BriefArticle, then write a trivial type-checker that processes them.

@fzyzcjy
Copy link
Author

fzyzcjy commented May 13, 2020

Er sorry I do not quite get it... How do I write a "trivial type-checker", do you mean extending the existing Checker Framework?

@mernst
Copy link
Member

mernst commented May 13, 2020

Yes. The process is explained at https://checkerframework.org/manual/#creating-a-checker .

@fzyzcjy
Copy link
Author

fzyzcjy commented May 18, 2020

Thanks very much!

@mernst mernst closed this as completed Jun 15, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants