Su axioma no es realmente un axioma, le faltan hipótesis. Las presentaciones simples de lógica de Hoare manipulan fórmulas de la forma donde y son fórmulas lógicas y es un comando. Es necesario asegurarse de que esté bien formado . En lenguajes simples como los que se usan a menudo para una primera introducción a la lógica de Hoare, la buena formación es sintáctica: generalmente es cuestión de verificar que{P}C{P′}PP′CCCse ajusta a una gramática libre de contexto y posiblemente a que las variables libres están dentro de un conjunto permitido. Si el lenguaje incluye construcciones que tienen una corrección semántica, como los accesos a los elementos de la matriz, debe agregar hipótesis para expresar esta corrección semántica.
Formalmente, puede agregar juicios para expresar la corrección de expresiones y comandos. Si las expresiones no tienen efectos secundarios, no necesitan condiciones posteriores, solo condiciones previas. Por ejemplo, puede escribir reglas de buena forma, como
y solo permite expresiones bien formadas en los comandos:
{P}E wf{P∧0≤E<length(A)}A[E] wf{P}E1 wf{P}E2 wf{P}E1+E2 wf
{P[x←E]}E wf{P[x←E]}x:=E{P}
Un enfoque diferente es tratar todas las expresiones como bien formadas, pero hacer que cualquier expresión que implique un cálculo mal formado tenga un valor especial . En idiomas con comprobación de límites de tiempo de ejecución, significa que "este programa generó una excepción fatal". A continuación, haría un seguimiento de si un programa se equivocó a través de un predicado lógico ; un programa solo es válido si puede probar que su condición posterior implica .
errorerrorError¬Error
{P[x←E]}x:=E{P∨Error}P[x←E]⟹E↛error{P[x←E]}x:=E{P}
Otro enfoque es considerar un Hoare triple para mantener solo si el programa termina correctamente. Este es el enfoque habitual para los programas que no terminan: la condición posterior se cumple cuando finaliza el comando, lo que puede no ocurrir siempre. Si trata los errores de tiempo de ejecución como no terminación, barre todos los problemas de corrección bajo el capó. Aún tendrá que demostrar la corrección del programa de alguna manera, pero no es necesario que esté en la lógica de Hoare si prefiere algún otro formalismo para esa tarea.
Por cierto, tenga en cuenta que expresar lo que sucede cuando se modifica una variable compuesta, como una matriz, está más involucrado que lo que escribió. Supongamos que era, por ejemplo, : la sustitución no cambiaría , sin embargo, la asignación podría invalidar . Incluso si restringe la sintaxis de los predicados para hablar solo de átomos, considere la asignación bajo la condición previa : no puede hacer una simple sustitución para obtener la condición posterior correcta , necesita evaluarPIsSorted(A)A[i]←EPA[i]←PPA[A[0]−1]:=A[0]A[0]=2∧A[1]=3A[0]=1∧A[1]=1A[0](lo que puede ser difícil en general, ya que la condición previa podría no especificar un solo valor posible para ). realizar la sustitución en la matriz: . Las notas de clase de Mike Gordon tienen una buena presentación lógica de Hoare con matrices (pero sin verificación de errores).A[0]A←A[i←E]
length
aA
?length
se renombróA_length
). Segundo, necesitamos axiomas de "creación" de matriz comoint[] a = int[length] {a_length==length}
. Creo que esto debería ser suficiente.