DOMANDA Semantica vettori

[aleio1]

Ciao a tutti, ho una domanda. Se volessi scrivere la semantica degli array come dovrei procedere?
Forse è una domanda troppo generica, ma non so come sviluppare il tutto.

Ho pensato che potrei esprimere gli array come una coppia (dim,fun:{0,...dim-1}->tipo) dove 'dim' è un intero che indica la dimensione e 'tipo' è il tipo degli elementi dell'array (diciamo interi).

Per accedere ad un elemento ho una seconda funzione che dato un indice i mi restituisce fun(i) se 0<=i<dim e mi dà errore altrimenti.

E' corretto?
E poi? Cosa mi serve più?
Grazie mille:)

 

[wolf1792]

sì direi che è corretto...
ma non ho capito cosa devi fare...

 

[aleio1]

Innanzitutto grazie infinite per avermi risposto.
Il punto è che, per come mi viene posta la domanda, non saprei essere molto preciso.

Sto studiando la semantica operazionale e denotazionale di un semplice linguaggio di programmazione che contiene
tipi: interi + booleani
istruzioni: assegnamento + skip + composizione di istruzioni + ifthenelse + while + chiamata procedure + blocchi (begin Dvar, Dproc, istruzione, end)
dichiarazioni: Dvar (dichiarazione di variabili), Dproc (dichiarazione di procedure)

Per ogni istruzione ovviamente ho una funzione semantica che prende un argomento e restituisce una funzione che manda uno stato in un altro (ovviamente funzioni diverse a seconda che io stia definendo una semantica denotazionale o operazionale). Ci sarebbero da introdurre i concetti di ambiente e locazioni ma per riassumere non li ho scritti.

Suppongo che la domanda sia: Abbiamo questo linguaggio con la sua semantica. Vogliamo inserire gli array in questo linguaggio. Come dovrei definire la loro semantica?

Ecco, la mia risposta intuitiva sarebbe quella che ho scritto nel mio primo post, ma non saprei come essere rigoroso.
Grazie a chiunque possa e voglia darmi una mano:)