I am attempting to formalise Java in Object-Z. The basic constructs (class, field, method) are mapped naturally to Object-Z. However, I could find no equivalence of Java's annotation in Object-Z.
That is, we would like to define for class, field and method with annotations.
So my questions are:
1/ Does Object-Z support annotation?
2/ If not, can it be extended to support annotation (perhaps according to the discussion in the paper "CZT Support for Z Extensions" by Tim Miller, Leo Freitas, Petra Malik, and Mark Utting)?
If Yes, how?
Thank you very much for your support.
David
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
I am attempting to formalise Java in Object-Z. The basic constructs (class, field, method) are mapped naturally to Object-Z. However, I could find no equivalence of Java's annotation in Object-Z.
That is, we would like to define for class, field and method with annotations.
Out of interest, have you seen the work done in Isabelle on formalising Java? You might get good ideas there.
So my questions are:
1/ Does Object-Z support annotation?
Not that I am aware of; but the underlying encoding of Object-Z (and CZT terms in general) allow for generalised term annotation with whatever you like.
For example, Location annotations for all terms from the parser, or type annotations for all terms from the type checker so that later top-level user tools
can quickly and easily refer to location or type information without the need to type check on the fly.
Other tools add this facility in different ways. Extending it to cope with what you want should be trivial; extending the parser to allow for user-based annotations
could take some work but I can’t see it being difficult as it wouldn’t generate parsing conflicts.
2/ If not, can it be extended to support annotation (perhaps according to the discussion in the paper "CZT Support for Z Extensions" by Tim Miller, Leo Freitas, Petra Malik, and Mark Utting)?
If Yes, how?
Thank you very much for your support.
David
Hope that helps. Let me know if you want to undertake this and I can try to help you around the sources.
Thank you very much for your information. Your answers do help to support my initial theory (still needs to be validated) that Object-Z can be extended to support user-based annotations (at least for class, state variable, and operation).
I will investigate this further and let you know.
Just curious, it seems that the CZT source code repository has not been updated for a while. Is it still active?
Best,
David.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Hi,
I am attempting to formalise Java in Object-Z. The basic constructs (class, field, method) are mapped naturally to Object-Z. However, I could find no equivalence of Java's annotation in Object-Z.
That is, we would like to define for class, field and method with annotations.
So my questions are:
1/ Does Object-Z support annotation?
2/ If not, can it be extended to support annotation (perhaps according to the discussion in the paper "CZT Support for Z Extensions" by Tim Miller, Leo Freitas, Petra Malik, and Mark Utting)?
If Yes, how?
Thank you very much for your support.
David
Hi,
On 4 Oct 2016, at 00:43, David Le dmle@users.sf.netamp#100;amp#109;amp#108;amp#101;amp#64;amp#117;amp#115;amp#101;amp#114;amp#115;amp#46;amp#115;amp#102;amp#46;amp#110;amp#101;amp#116; wrote:
Hi,
I am attempting to formalise Java in Object-Z. The basic constructs (class, field, method) are mapped naturally to Object-Z. However, I could find no equivalence of Java's annotation in Object-Z.
That is, we would like to define for class, field and method with annotations.
Out of interest, have you seen the work done in Isabelle on formalising Java? You might get good ideas there.
So my questions are:
1/ Does Object-Z support annotation?
Not that I am aware of; but the underlying encoding of Object-Z (and CZT terms in general) allow for generalised term annotation with whatever you like.
For example, Location annotations for all terms from the parser, or type annotations for all terms from the type checker so that later top-level user tools
can quickly and easily refer to location or type information without the need to type check on the fly.
Other tools add this facility in different ways. Extending it to cope with what you want should be trivial; extending the parser to allow for user-based annotations
could take some work but I can’t see it being difficult as it wouldn’t generate parsing conflicts.
2/ If not, can it be extended to support annotation (perhaps according to the discussion in the paper "CZT Support for Z Extensions" by Tim Miller, Leo Freitas, Petra Malik, and Mark Utting)?
If Yes, how?
Thank you very much for your support.
David
Hope that helps. Let me know if you want to undertake this and I can try to help you around the sources.
Best,
Leo
Can Object-Z support annotation (similar to Java's annotation)?https://sourceforge.net/p/czt/discussion/295268/thread/af0659f3/?limit=25#f8a8
Sent from sourceforge.nethttp://sourceforge.net because you indicated interest in https://sourceforge.net/p/czt/discussion/295268/
To unsubscribe from further messages, please visit https://sourceforge.net/auth/subscriptions/
Dear Leo,
Thank you very much for your information. Your answers do help to support my initial theory (still needs to be validated) that Object-Z can be extended to support user-based annotations (at least for class, state variable, and operation).
I will investigate this further and let you know.
Just curious, it seems that the CZT source code repository has not been updated for a while. Is it still active?
Best,
David.