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.

Apache HTTP Server + Glassfish Open Source Edition v3, vía AJP

Sí, sé que hay mucha información en San Google, pero resulta que TODOS los foros, blogs, manuales y demás que seguí decían práticamente lo mismo para realizar tal configuración, no obstante seguí las instrucciones, las repasé una y otra vez y ¡nada!

Bueno, sin postear TODO el proceso (pues prácticamente pueden encontrarlo de manera bastante fácil, sólo usen Google o su buscador favorito) sólo les comento y les aconsejo que cuando vean que algo no les da el resultado que desean (en mi caso con el Glassfish, y en general, me imagino que aplica para cualquier servidor), lo que debería ser y después claro de haber repasado una y otra y otra y otra vez, entonces, MODIFIQUEN MANUALMENTE EL ARCHIVO DE CONFIGURACIÓN para agregar las líneas necesarias y NO SE CONFIEN TANTO DE LA INTERFAZ GRÁFICA del servidor (si es que lo hay a disposición), en mi caso fue el Glassfish: prácticamente tuve que re-escribir unas líneas que ya había en ${GLASSFISH_HOME}/domains/domain1/config.xml referente a lo de habilitar el puerto 8009 (AJP) para Glassfish.

En fin, espero algún día poder detallar el proceso completo y cuál exactamente fue el error y cómo lo resolví. Mientras tanto tomen mi consejo pues muchas veces (más bien TODAS las veces) tendremos que lidiar con los interiores de los gigantes para poder entenderlos, mientras tanto, sólo conocemos su exterior que no siempre es la puerta correcta para hacer las cosas.