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.