Significato dell'utilizzo di BitVectors per modellare i numeri interi per l'account per l'overflow

Question

Significato dell'utilizzo di BitVectors per modellare i numeri interi per l'account per l'overflow

#1 da (3 voti)
#2 da (0 voti)

1

Ho appena rilevato questa frase:

Depending on the context, we may prefer to model integers as bitvectors rather than mathematical integers, since the Int type does not model overflow.

Mi chiedo cosa significhi. Sono nuovo nell'apprendimento di overflow di interi . Ti chiedi cosa significa modellare gli interi come bitvector e come lo faresti. E poi come questo ti permetterebbe di considerare l'overflow (chiedendoti se dovresti scrivere dei test per qualche tipo, o è in qualche modo implicito nel modello). È intrigante l'idea di modellare gli interi in modo che tengano conto dei problemi del mondo reale come gli overflow integer. Forse se potesse essere delineato usando JavaScript come esempio che mi è familiare sarebbe utile.

Un altro articolo dice qualcosa di simile:

Overflows are a common source of programming errors, which makes it crucial to model them accordingly. In the theory of fixed-size bitvectors, overflow effects are directly modeled by the semantics of its function symbols and require no extra encoding constraints. These properties make bitvector logic a perfect fit for many verification purposes, especially in the field of low-level programming.

javascript bit model

posta Lance Pollard 22.07.2018 - 02:34

fonte

2 risposte

0

Questo è più facile da capire con interi senza segno e la risposta è essenzialmente la stessa.

Inoltre, gli interi senza segno sono disponibili in diverse dimensioni, ma per semplificare la presentazione assumerò interi a 32 bit.

Potresti ricordare nell'apprendimento della scuola elementare sulla nozione del valore del luogo e sui numeri in diverse basi. Nella scuola elementare ci hanno insegnato che 213 erano 2 x 100 + 1x10 + 3x1. Tu rappresenti un numero come la somma di una serie di fattori moltiplicati per dieci.

Potresti aver visto anche basi generalizzate su basi diverse (come base 8 o base 5 o base 16).

Bene, il modo in cui i numeri sono tipicamente rappresentati nei moderni computer digitali è la base 2 (nota anche come binario).

Quindi 1001 significa 1x2x2x2 + 0x2x2 + 0x2 + 1 × 1 (mi dispiace non è possibile digitare esponenti su questa tastiera).

Quindi qualsiasi numero intero non negativo può essere rappresentato come una serie di uno o zero (spesso chiamati bit), dove il valore del numero è la somma come sopra (notazione del valore di base del 2 posto).

Ora, se si sceglie di rappresentare i propri numeri con un numero fisso di cifre (32 e 64 sono scelte comuni), quando si eseguono operazioni aritmetiche si può finire con un numero che non si adatta (> = 2 pow (32 ) nel nostro caso). Questo è un overflow.

In genere il vettore di parole in computerese si riferisce a un array le cui dimensioni sono determinate in fase di esecuzione per essere sufficientemente grandi.

Se invece di rappresentare numeri con un numero fisso di bit lo si fa con una matrice di bit (vector) allocata dinamicamente, non si ha overflow. A parte queste rappresentazioni di numeri allocate dinamicamente vengono solitamente chiamate bignum.

risposta data 22.07.2018 - 03:16

fonte

Leggi altre domande sui tag javascript bit model

Topologia di rete per sistemi ATM e POS Quando si definisce la mappa del testo locale, la chiave della lingua o la chiave di testo, quale dovrebbe essere la prima chiave?

score 3 · Accepted Answer

La cosa che molti linguaggi di programmazione chiamano "interi" non sono in realtà numeri interi, ma bitvettori a dimensione fissa interpretati come numeri interi ... ma poiché sono di dimensione fissa, possono "overflow", il che significa che il risultato di un calcolo può essere più grande di quello che si adatta al bitvector a dimensione fissa.

Tutta quella frase sta dicendo che dal momento che i linguaggi di dimensione fissa (in linguaggio di programmazione) sono bitvector a dimensione fissa in un linguaggio di programmazione reale, dovremmo anche modellarli come fissi -misura bitvector nel nostro linguaggio delle specifiche e prova invece di modellarli come interi (matematicamente ideali) che si comportano in modo diverso.

In particolare, l'overflow dei numeri interi può essere una fonte comune di bug, quindi modellare le proprietà di sicurezza di un sistema, ma ignorare una fonte comune di bug non ha senso.