Loop invariance insertion sort algorithm I have the following pseudo code for a insertion sort algorithm
INSERTION-SORT

1 for j = 2 to A.length
2    key = A[j]
3    // Insert A[j] into the sorted sequence A[1..j-1]
4    i = j -1 
5    while i &gt; 0 and A[i] &gt; key
6        A[i+1] = A[i]
7         i = i -1
8    A[i+1] = key

I am trying to convert it into executable code written in Python
def main():
    A = [5,2,4,6,1,3]
    for j in range(1,len(A)):
        key = A[j]
        i = j - 1
        while i &gt;= 0 and A[i] &gt; key:
            A[i + 1] = A[i]
            i = i - 1
        A[i + 1] = key
        print A[0:j+1]
    return A
 
main()

is this a correct translation? I'm not sure if I messed something up with the indexes because it seems as though I'm not getting the end index with range. Furthermore I'm going to be testing correctness with initialization, maintenance and termination.
I added the line print A[0:j] to show initialization and maintenance but I'm not sure if it should be print A[0:j-1].
Any help is greatly appreciated!
Python arrays have 0-based indexing, like in C, and unlike Fortran, which uses 1-based indexing. You can check Wikipedia for information about other languages.
A python array $A$ of length $n$ consists of the elements $A[0],\ldots,A[n-1]$. The python function range(n) goes over the indices $0,\ldots,n-1$, and your range(1,n) goes over the indices $1,\ldots,n-1$.
In insertion sort, we go over all prefixes of the array inductively, and make sure that they are sorted. If $A[0],\ldots,A[j-1]$ is already sorted, in order to make $A[0],\ldots,A[j]$ sorted, we just need to more the current $A[j]$ into its proper location. Since $A[0]$ is automatically sorted, we only need to go over $j=1,j=2,\ldots,j=n-1$, at which point the entire array $A[0],\ldots,A[n-1]$ is sorted. This is why the loop goes over range(1,n).
Is your implementation correct? Practically speaking, the best way to find out is to test it on many inputs. While such a test cannot verify that the algorithm is correct, and could miss some corner cases, it is also likely to catch off-by-one errors, especially in a language like python with bounds checking. Since insertion sort is such a simple algorithm, you are likely to catch any implementation errors by sorting small random arrays.