Un file .dex è il formato di trasporto per il bytecode Dalvik. Esistono determinati vincoli sintattici e semantici per fare in modo che un file sia un file .dex valido ed è necessario un runtime per supportare solo file .dex validi.
Vincoli generali di integrità dei file .dex
I vincoli di integrità generali riguardano la struttura più grande di un
    file .dex, come descritto in dettaglio nel formato .dex.
| Identificatore | Descrizione | 
|---|---|
| G1 | Il numero magicdel file.dexdeve esseredex\n035\0per la versione 35 o simile per le versioni successive. | 
| G2 | Il checksum deve essere un checksum Adler-32 dell'intero contenuto del file
          tranne i campi magicechecksum. | 
| G3 | La firma deve essere un hash SHA-1 dell'intero contenuto del file, ad eccezione di magic,checksumesignature. | 
| G4 | 
 
 | 
| G5 | 
 
 | 
| G6 | endian_tagdeve avere il valore:ENDIAN_CONSTANToREVERSE_ENDIAN_CONSTANT | 
| G7 | Per ogni sezione  
            I campi  | 
| G8 | Tutti i campi di offset nell'intestazione, tranne map_off, devono essere allineati a quattro byte. | 
| G9 | Il campo map_offdeve essere pari a zero o fare riferimento alla sezione dei dati. In quest'ultimo caso, la sezionedatadeve esistere. | 
| G10 | Nessuna delle sezioni link,string_ids,type_ids,proto_ids,field_ids,method_ids,class_defsedatadeve sovrapporsi l'una all'altra o all'intestazione. | 
| G11 | Se esiste una mappa, ogni voce della mappa deve avere un tipo valido. Ogni tipo può essere visualizzato al massimo una volta. | 
| G12 | Se esiste una mappa, ogni voce della mappa deve avere un offset e una dimensione diversi da zero. L'offset deve puntare alla sezione corrispondente del file (ad es. un string_id_itemdeve puntare alla sezionestring_ids) e le dimensioni esplicite o
          implicite dell'elemento devono corrispondere ai contenuti e alle dimensioni effettivi della
          sezione. | 
| G13 | Se esiste una mappa, l'offset della voce della mappa n+1deve essere maggiore o uguale all'offset della voce della mappan plus than size of map entry n. Ciò implica voci non sovrapposte e ordinamento da basso a alto. | 
| G14 | I seguenti tipi di voci devono avere un offset alinhato su quattro byte: string_id_item,type_id_item,proto_id_item,field_id_item,method_id_item,class_def_item,type_list,code_item,annotations_directory_item. | 
| G15 | Per ogni  Per ogni   Per  | 
| G16 | Per ogni type_id_item, il campodescriptor_idxdeve contenere un riferimento valido all'elencostring_ids. La stringa a cui si fa riferimento deve essere un descrittore di tipo valido. | 
| G17 | Per ogni proto_id_item, il camposhorty_idxdeve contenere un riferimento valido all'elencostring_ids. La stringa a cui si fa riferimento deve essere un descrittore shorty valido. Inoltre, il camporeturn_type_idxdeve essere un indice valido della sezionetype_idse il campoparameters_offdeve essere zero o un offset valido che rimandi alla sezionedata. Se diverso da zero, l'elenco dei parametri
          non deve contenere voci vuote. | 
| G18 | Per ogni field_id_item, sia i campiclass_idxsiatype_idxdevono essere
          indici validi nell'elencotype_ids. La voce a cui fa riferimentoclass_idxdeve essere un tipo di riferimento non array. Inoltre, il camponame_idxdeve essere un
          riferimento valido alla sezionestring_idse i contenuti della voce di riferimento
          devono essere conformi alla specificaMemberName. | 
| G19 | Per ogni method_id_item, il campoclass_idxdeve essere un indice valido
          nella sezionetype_idse la voce a cui si fa riferimento deve essere un tipo di riferimento
          non array. Il campoproto_iddeve essere un riferimento valido nell'elencoproto_ids. Il camponame_idxdeve essere un riferimento valido alla sezionestring_idse i contenuti della voce a cui si fa riferimento devono essere conformi alla specificaMemberName. | 
| G20 | Per ogni field_id_item, il campoclass_idxdeve essere un indice valido
          nell'elencotype_ids. La voce a cui si fa riferimento deve essere di tipo
          riferimento non array. | 
Vincoli del bytecode statico
I vincoli statici sono vincoli sui singoli elementi del bytecode. In genere possono essere controllati senza utilizzare tecniche di controllo o analisi del flusso di dati.
| Identificatore | Descrizione | 
|---|---|
| A1 | L'array insnsnon deve essere vuoto. | 
| A2 | Il primo opcode nell'array insnsdeve avere indice zero. | 
| A3 | L'array insnsdeve contenere solo opcode Dalvik validi. | 
| A4 | L'indice dell'istruzione n+1deve essere uguale all'indice dell'istruzionenpiù la lunghezza dell'istruzionen, tenendo conto dei possibili operandi. | 
| A5 | L'ultima istruzione nell'array insnsdeve terminare all'indiceinsns_size-1. | 
| A6 | Tutti i target gotoeif-<kind>devono essere opcode all'interno dello stesso metodo. | 
| A7 | Tutti i target di un'istruzione packed-switchdevono essere
          opcode all'interno dello stesso metodo. Le dimensioni e l'elenco di target devono essere coerenti. | 
| A8 | Tutti i target di un'istruzione sparse-switchdevono essere
          opcode all'interno dello stesso metodo. La tabella corrispondente deve essere
          coerente e ordinata dal più basso al più alto. | 
| A9 | L'operando Bdelle istruzioniconst-stringeconst-string/jumbodeve essere un indice valido
          nel pool di costanti di stringa. | 
| A10 | L'operando Cdelle istruzioniiget<kind>eiput<kind>deve essere un indice valido nel
          pool di costanti dei campi. La voce a cui si fa riferimento deve rappresentare un
          campo istanza. | 
| A11 | L'operando Cdelle istruzionisget<kind>esput<kind>deve essere un indice valido nel
          pool di costanti dei campi. La voce a cui si fa riferimento deve rappresentare un campo statico. | 
| A12 | L'operando Cdelle istruzioniinvoke-virtual,invoke-super,invoke-directeinvoke-staticdeve essere un indice valido nel
          pool di costanti del metodo. | 
| A13 | L'operando Bdelle istruzioniinvoke-virtual/range,invoke-super/range,invoke-direct/rangeeinvoke-static/rangedeve essere un indice valido
          nel pool di costanti del metodo. | 
| A14 | Un metodo il cui nome inizia con un "<" deve essere invocato solo implicitamente dalla VM, non dal codice proveniente da un file .dex. L'unica eccezione è l'inizializzatore dell'istanza, che può essere invocato dainvoke-direct. | 
| A15 | L'operando Cdell'istruzioneinvoke-interfacedeve essere un indice valido nel pool di costanti del metodo. Il
          valoremethod_ida cui viene fatto riferimento deve appartenere a un'interfaccia (non a un
          oggetto). | 
| A16 | L'operando Bdell'istruzioneinvoke-interface/rangedeve essere un indice valido nel pool di costanti del metodo.
          Il riferimento amethod_iddeve appartenere a un'interfaccia (non a un
          corso). | 
| A17 | L'operando Bdelle istruzioniconst-class,check-cast,new-instanceefilled-new-array/rangedeve essere un indice valido
          nel pool di costanti di tipo. | 
| A18 | L'operando Cdelle istruzioniinstance-of,new-arrayefilled-new-arraydeve essere un indice valido nel pool di costanti di tipo. | 
| A19 | Le dimensioni di un array creato da un'istruzione new-arraydevono essere inferiori a256. | 
| A20 | L'istruzione newnon deve fare riferimento a classi di array,
          interfacce o classi astratte. | 
| A21 | Il tipo a cui fa riferimento un'istruzione new-arraydeve essere
          un tipo valido non di riferimento. | 
| A22 | Tutti i registri a cui fa riferimento un'istruzione in modalità singola larghezza
          (non a coppie) devono essere validi per il metodo corrente. In altre parole,
          i relativi indici devono essere non negativi e inferiori a registers_size. | 
| A23 | Tutti i registri a cui fa riferimento un'istruzione in modalità a doppia larghezza (coppia) devono essere validi per il metodo corrente. In altre parole, i relativi indici
          devono essere non negativi e inferiori a registers_size-1. | 
| 24A | L'operando method_iddelle istruzioniinvoke-virtualeinvoke-directdeve appartenere a una classe
          (non a un'interfaccia). Nei file Dex precedenti alla versione037deve valere lo stesso per le istruzioniinvoke-supereinvoke-static. | 
| A25 | L'operando method_iddelle istruzioniinvoke-virtual/rangeeinvoke-direct/rangedeve appartenere a una classe
          (non a un'interfaccia). Nei file Dex precedenti alla versione037deve valere lo stesso per le istruzioniinvoke-super/rangeeinvoke-static/range. | 
Vincoli del bytecode strutturale
I vincoli strutturali sono vincoli sulle relazioni tra diversi elementi del bytecode. In genere non possono essere controllati senza impiegare tecniche di controllo o di analisi del flusso di dati.
| Identificatore | Descrizione | 
|---|---|
| B1 | Il numero e i tipi di argomenti (registri e valori immediati) devono sempre corrispondere all'istruzione. | 
| B2 | Le coppie di registri non devono mai essere suddivise. | 
| B3 | Prima di poter essere letto, un registro (o una coppia) deve essere assegnato. | 
| B4 | Un'istruzione invoke-directdeve invocare un inizializzatore di istanza o un metodo solo nella classe corrente o in una delle sue superclassi. | 
| B5 | Un inizializzante dell'istanza deve essere invocato solo su un'istanza non inizializzata. | 
| B6 | I metodi di istanza possono essere invocati solo su ed è possibile accedere ai campi di istanza solo su istanze già inizializzate. | 
| B7 | Un registro che contiene il risultato di un'istruzione new-instancenon deve essere utilizzato se la stessa
          istruzionenew-instanceviene eseguita di nuovo prima
          dell'inizializzazione dell'istanza. | 
| B8 | Un inizializzante dell'istanza deve chiamare un altro inizializzante dell'istanza (stessa
           classe o superclasse) prima che sia possibile accedere ai membri dell'istanza.
           Le eccezioni sono campi di istanze non ereditati, che possono essere assegnati
           prima di chiamare un altro inizializzante e la classe Objectin generale. | 
| B9 | Tutti gli argomenti effettivi del metodo devono essere compatibili con l'assegnazione con i rispettivi argomenti formali. | 
| B10 | Per ogni chiamata al metodo dell'istanza, l'istanza effettiva deve essere compatibile con l'assegnazione con la classe o l'interfaccia specificata nell'istruzione. | 
| B11 | Un'istruzione return<kind>deve corrispondere al
           tipo di ritorno del metodo. | 
| B12 | Quando accedi ai membri protetti di una superclasse, il tipo effettivo dell'istanza a cui si accede deve essere la classe corrente o uno dei suoi sottoclassi. | 
| B13 | Il tipo di un valore memorizzato in un campo statico deve essere compatibile con l'assegnazione o convertibile nel tipo del campo. | 
| B14 | Il tipo di un valore memorizzato in un campo deve essere compatibile con l'assegnazione o convertibile nel tipo del campo. | 
| B15 | Il tipo di ogni valore memorizzato in un array deve essere compatibile con l'assegnazione del tipo di componente dell'array. | 
| B16 | L'operando Adi un'istruzionethrowdeve essere compatibile con l'assegnazione conjava.lang.Throwable. | 
| B17 | L'ultima istruzione raggiungibile di un metodo deve essere un gotoo un ramo a ritroso, unreturno un'istruzionethrow. Non deve essere possibile lasciareinsnsin fondo all'array. | 
| B18 | La metà non assegnata di una coppia di registri precedente non può essere letta (è considerata non valida) finché non viene riassegnata da un'altra istruzione. | 
| B19 | Un'istruzione move-result<kind>deve essere immediatamente
          preceduta (nell'arrayinsns) da un'istruzioneinvoke-<kind>. L'unica eccezione è
          l'istruzionemove-result-object, che può anche essere
          preceduta da un'istruzionefilled-new-array. | 
| B20 | Un'istruzione move-result<kind>deve essere immediatamente
          preceduta (nel flusso di controllo effettivo) da un'istruzionereturn-<kind>corrispondente (non deve essere eseguita un salto
          a questa istruzione). L'unica eccezione è l'istruzionemove-result-object, che può essere preceduta anche da un'istruzionefilled-new-array. | 
| B21 | Un'istruzione move-exceptiondeve apparire solo come
          prima istruzione in un gestore delle eccezioni. | 
| B22 | Le pseudo-istruzioni packed-switch-data,sparse-switch-dataefill-array-datanon devono essere raggiungibili dal flusso di controllo. | 
