Mathematical formulations for linked lists

Hello to everybody! I'm working with my master thesis based on verification and validation external using Design By Contract for Java. Specifically checking JML specifications, so I have one question about JML specifications, any help would be appreciated.

Question

For the case of LinkedList's JML specifications, Does anyone know where can I get the mathematical expressions for these specifications? I've really looked in (just are some, of course I google it!):

• "The logic theory machine, a complex information processing system" by Allen Newell and Herbert A. Simon,
• "The Art of Computer Programming" by Donald E. Knuth and
• "Abstract data types: specifications, implementations, and applications" by Nell Dale and Henry M. Walker.

Specifically looking the mathematical expressions for the methods (e.g. add(int, Object), Object get(int), etc.). I understand that the specifications really are written in JML, but someone wants the specification in mathematical expressions, the arguments are that "mathematical expressions aren't ambiguos" and then can be prove them by formal methods.

Changing my posts to english

I'm considering change my posts (and my tweets too) to english. Some reasons to do this are:

• Open my scope (people from anywhere can read and understand my posts, not only lationamerica)
• The lack of comments to my posts (maybe the main reason is the previous one)
• Doing this, change the idiom for my posts, I can practice the writing for my article that I have to write to get my master

If anyone has any comment, please write it. Any doubts, or advices will be wellcome.