Obtain the name of the elastic beanstalk autoscaling group

It is possible to export the name of the autoscaling group which elastic beanstalk provisions as part of each elastic beanstalk environment. This exported value can then be used from other cloud formation stacks in order to add custom scaling triggers, etc. We can export values by adding an outputs section into a .ebextensions file.

If you have large numbers of stacks it is very helpful if one can use a consistent naming scheme for the exported values. There is a way to pass a namespace into elastic beanstalk by using a custom option.

Here is the CloudFormation yaml to be included in an elastic beanstalk extension file:

Parameters:
  BeanstalkASGName:
    Type: String
    Description: "The name to export the autoscaling group name under"
    Default:
      Fn::GetOptionSetting:
        OptionName: MyBeanstalkStackInfoName
        DefaultValue: unknown
Outputs:
  OutputAutoScalingGroupName:
    Description: Beanstalk AutoScalingGroup Name
    Value:
      Ref: "AWSEBAutoScalingGroup"
    Export:
      Name:
        Fn::Join:
          - "-"
          - - { "Ref" : "BeanstalkASGName" }
            - "AutoScalingGroup"

Note that Fn::GetOptionSetting does not seem to be allowed directly in the Outputs section. So we have to use it instead to set the value of a parameter in a Parameters section, and then use the value indirectly via the parameter.

Here is a snippet to use in your master CloudFormation file:

Namespace: aws:elasticbeanstalk:customoption
OptionName: MyBeanstalkStackInfoName
Value: anyvalue

Cloudformation example of an S3 bucket with attached SQS notifications

Creating an s3 bucket with an SQS queue attached is a simple and powerful configuration. Cloudformation allows one to express such a configuration as code and commit it to a git repository. I was not able to find a complete example of how to express such a configuration using Cloudformation. What follows is written using the Troposhere library. Please do not take this post to be an endorsement of using Troposhere.

t = self.template
 
# The queue which will handle the S3 event messages
t.add_resource(Queue(
    "MyQueue",
    VisibilityTimeout=30,
    MessageRetentionPeriod=60,
    QueueName=Sub("my-${AWS::Region}-${AWS::AccountId}")
))
 
# The bucket that will generate the s3 events. The NotificationConfiguration
# also supports SNS and Lambda. Notifications can also be filtered according
# the S3 key of the object to which the event relates.
t.add_resource(Bucket(
    "MyBucket",
    BucketName=Sub("my-${AWS::Region}-${AWS::AccountId}"),
    # Note that the queue policy must be created first
    DependsOn="MyQueuePolicy",
    NotificationConfiguration=NotificationConfiguration(
        QueueConfigurations=[
            QueueConfigurations(
                Event="s3:ObjectCreated:*",
                Queue=GetAtt("MyQueue", "Arn"),
            )
        ]
    )
))
 
# The queue policy will give access to the S3 bucket to send on the queue
# The queue policy can also be used to give permission to the message receiver
t.add_resource(QueuePolicy(
    "MyQueuePolicy",
    Queues=[Ref("MyQueue")],
    PolicyDocument={
        "Version": "2012-10-17",
        "Statement": [
            # Allow the S3 bucket to publish to the queue
            # https://docs.aws.amazon.com/AmazonS3/latest/dev/NotificationHowTo.html#grant
            # -destinations-permissions-to-s3
            {
                "Effect": "Allow",
                "Principal": Principal("Service", ["s3.amazonaws.com"]),
                "Action": [
                    "SQS:SendMessage"
                ],
                "Resource": GetAtt("MyQueue", "Arn"),
                "Condition": {
                    "ArnLike": {
                        # have to construct the ARN from the static bucket name to avoid
                        # the circular dependency
                        # https://aws.amazon.com/premiumsupport/knowledge-center/unable-validate-destination-s3/
                        "aws:SourceArn": Join("", [
                            "arn:aws:s3:::",
                            Sub("my-${AWS::Region}-${AWS::AccountId}")
                        ])
                    }
                }
            },
            # Allow some user to read from the queue. This is just and example,
            # please change this to match the permissions your use case requires.
            {
                "Effect": "Allow",
                "Principal": AWSPrincipal(GetAtt("MyUser", "Arn")),
                "Action": [
                    "sqs:ReceiveMessage"
                ],
                "Resource": GetAtt("MyQueue", "Arn"),
            }
        ]
    }
))
 
# Allow some user to manipulate the S3 bucket. This is just and example,
# please change this to match the permissions your use case requires.
t.add_resource(BucketPolicy(
    "MyBucketPolicy",
    Bucket=Ref("MyBucket"),
    PolicyDocument={
        "Version": "2012-10-17",
        "Statement": [
            {
                "Effect": "Allow",
                "Principal": AWSPrincipal(GetAtt("MyUser", "Arn")),
                "Action": [
                    "s3:GetObject",
                    "s3:PutObject",
                    "s3:DeleteObject"
                ],
                "Resource": Join("", [GetAtt("MyBucket", "Arn"), "/*"])
            }
        ]
    }
))

Server-to-Server authentication for the Microsoft Dynamics web API

To connect to the Microsoft Dynamics web API from another server you can use OAuth v2.0 with the client_credentials grant. Making request to obtain the OAuth token is very simple.

The tenant ID is obtained from the azure portal, under manage properties and is indicated as the directory ID

You can obtain the value for the scope from the dynamics portal by visiting Settings > Customization > Developer Resources and looking at the service root URL.

requests.post(
      f'https://login.microsoftonline.com/{tenant}/oauth2/v2.0/token',
        data={
            'client_id': settings.DYNAMICS_CLIENT_ID,
            'scope': 'https://*********.api.crm*.dynamics.com/.default',
            'client_secret': settings.DYNAMICS_CLIENT_SECRET,
            'grant_type': 'client_credentials',
        }
    )

A number of steps are required to make this work.

Register an OAuth App in Azure AD

There is a walkthrough of registering an OAuth app on Azure AD. The essential process is to use the Active Directory section of the Azure management portal to register a new application, give it the Dynamics 365 (online)Delegated Permissions permission, and create a new secret for it.

Note that the redirect URI you enter doesn’t actually need to identify a real reachable resource.

Obtain Admin Consent for Dynamics 365

To obtain admin consent for the app, put the following URL in to a web browser. In the URL you must fill in the ID of the OAuth App you registered in the previous step, and also the redirect URI you registered for that App.

https://login.microsoftonline.com/{tenant}/adminconsent?client_id={your_client_id}&state=12345&redirect_uri={your_redirect_uri}

Configure a System User on Dynamics 365

In order to use your approved OAuth client you need to create a corresponding system user on Dynamics itself. This user does not require a license.

You need to create an appropriate security role for this user. Then create the user, ensuring that you select the Application user form. The Application ID must match the one that you registered with Azure. The strange padlock icon on some of the fields means that you should not fill them in because they will be looked up using the Application ID

NOTE: you may find it useful to give the security role the prvActOnBehalfOfAnotherUser permission to allow your service to impersonate other users.

You will also need to give the new system user sufficient permissions to take the actions that your application will perform. Both the system user and the impersonated user must have permissions in order for the action to be permitted.

Make Requests using the token

You should now be able to make requests using the token:

    api_root = 'https://********.api.crm*.dynamics.com/api/data/v9.0/'
 
    r = requests.get(
        api_root + 'systemusers',
        params={
            f"$filter": "internalemailaddress eq '{email}'",
            "$select": "internalemailaddress",
        },
        headers={
            'Authorization': 'Bearer ' + token,
        })

To impersonate a user you have to send a custom header with the correct ID for the particular user you want to impersonate. You can find the ID of a user using the request in the example above.

'MSCRMCallerID': systemuserid

Connecting SNS to a lambda function using CloudFormation

We are using Amazon CloudFormation to configure our infrastructure as code. We are doing video processing using a Lambda function triggered by a message in an SNS queue. The documentation on how to do this in CloudFormation is fairly poor. In this article I will show some troposphere code that shows how to do this.

First create the lambda function. This one just logs its invocation event into the cloudwatch logs:

def create_lambda(self):
    t = self.template
 
    code = [
        "exports.handler = function(event, context) {" +
        "    console.log(\"event: \", JSON.stringify(event, null, 4));" +
        "    context.succeed(\"success\");" +
        "}"
    ]
 
    return t.add_resource(Function(
        "LambdaFunction",
        Code=Code(
            ZipFile=Join("", code)
        ),
        Handler="index.handler",
        Role=GetAtt("LambdaExecutionRole", "Arn"),
        Runtime="nodejs4.3",
    ))

Creating the SNS topic is straightforward:

def subscribe_lambda_to_topic(self, topic, function):
    topic.Subscription = [Subscription(
        Protocol="lambda",
        Endpoint=GetAtt(function, "Arn")
    )]

The most complicated, and least well documented, part of the configuration is to give the relevant authorisations. The lambda function itself will require authorisation to use any resources it needs. In this example it is given authority to log to cloudwatch. It is also necessary to set a lambda permission that allows SNS to invoke the lambda in response to a message on the topic. Note that this permission is not a normal IAM role and policy, but something specific to lambda.

def give_permission_to_lambda(self, topic, function):
    t = self.template
 
    # This role gives the lambda the permissions it needs during execution
    lambda_execution_role = t.add_resource(Role(
        "LambdaExecutionRole",
        Path="/",
        AssumeRolePolicyDocument={"Version": "2012-10-17", "Statement": [
            {
                "Action": ["sts:AssumeRole"],
                "Effect": "Allow",
                "Principal": {
                    "Service": [
                        "lambda.amazonaws.com",
                    ]
                }
            }
        ]},
    ))
 
    lambda_execution_policy = t.add_resource(PolicyType(
        "LambdaExecutionPolicy",
        PolicyName="LambdaExecutionPolicy",
        PolicyDocument={
            "Version": "2012-10-17", "Statement": [
                {"Resource": "arn:aws:logs:*:*:*",
                 "Action": ["logs:*"],
                 "Effect": "Allow",
                 "Sid": "logaccess"}]},
        Roles=[Ref(lambda_execution_role)]
    ))
 
    t.add_resource(Permission(
        "InvokeLambdaPermission",
        FunctionName=GetAtt(function, "Arn"),
        Action="lambda:InvokeFunction",
        SourceArn=Ref(topic),
        Principal="sns.amazonaws.com"
    ))

Java code for generating permutations of a list using Heap’s algorithm

Java code for generating permutations of a list using Heap’s algorithm.

/**
 * Uses Heap's algorithm to produce all permutations of a given list.
 * We use an iterator to avoid having to use too much memory.
 *
 * @author t.wood
 *
 * Copyright 2016 Tim Wood
 *
 * Permission is hereby granted, free of charge, to any person 
 * obtaining a copy of this software and associated documentation 
 * files (the "Software"), to deal in the Software without restriction,
 * including without limitation the rights to use, copy, modify, merge,
 * publish, distribute, sublicense, and/or sell copies of the Software,
 * and to permit persons to whom the Software is furnished to do so, 
 * subject to the following conditions:
 * 
 * The above copyright notice and this permission notice shall be 
 * included in all copies or substantial portions of the Software.
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
 * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
 * IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
 * CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, 
 * TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE 
 * SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 * 
 * @param <T> The type of item being permuted
 * @param <R> The type resulting from decorating the permutation
 */
public final class PermutationIterator<T,R> implements Iterator<R> {
    private final Function<List<T>, R> defensiveDecorator;
    private final List<T> a;
    private R pending;
 
    private final int[] skel;
    private int i;
 
    /**
     * An iterator of permutations
     *
     * @param a the list to permute
     * @param decorator a decorator to apply to the permutation, a defensive copy
     *                  of the permutation is taken before it is passed to the decorator
     */
    public PermutationIterator(final List<T> a, final Function<List<T>,R> decorator) {
        defensiveDecorator = t -> decorator.apply(new ArrayList<>(t));
        pending = defensiveDecorator.apply(a);
        this.a = new ArrayList<>(a);
        skel = new int[a.size()];
        i = 0;
    }
 
    @Override public boolean hasNext() {
        return pending != null;
    }
 
    @Override public R next() {
        if(pending == null) {
            throw new IndexOutOfBoundsException();
        }
        final R result = pending;
        pending = permute();
        return result;
    }
 
    private R permute() {
        while(i < a.size()) {
            if (skel[i] < i) {
                if (even(i)) {
                    swap(a, 0, i);
                } else {
                    swap(a, skel[i], i);
                }
                skel[i] += 1;
                i = 0;
                return defensiveDecorator.apply(a);
            } else {
                skel[i] = 0;
                i += 1;
            }
        }
        return null;
    }
 
    private void swap(final List<T> a, final int i0, final int i1) {
        final T t = a.get(i0);
        a.set(i0, a.get(i1));
        a.set(i1, t);
    }
 
    private boolean even(final int i) {
        return i % 2 == 0;
    }
}

Notes on Structured Programming – Section 5, Remark 3

Here is a Dafny proof of the “exercise for the reader” from section 5 of E.W.Dijkstra’s “Notes on Structured Programming” monograph in the book “Structured Programming (1972)”.

method Section5RemarkThree(A:int, B:int) returns (z:int) 
  requires A > 0
  requires B >= 0
  ensures z == power(A,B)
{
  var x := A;
  var y := B;
  z := 1;
 
  while y != 0
    invariant x > 0
    invariant y >= 0
    invariant power(A, B) == z * power(x, y)
  {
    halfExponentSquareBase(x, if odd(y) then y-1 else y);
 
    if odd(y)
    {
      y := y - 1;
      z := z * x;
    }
    y := y/2;
    x := x * x;
  }
}
 
lemma halfExponentSquareBase(x:int,y:int)
  requires x > 0
  requires y >= 0
  requires even(y)
  ensures power(x, y) == power(x*x, y/2)
 {
   if y != 0 {
     halfExponentSquareBase(x,y-2);
   }
 }
 
predicate method even(n: nat)
   ensures even(n) <==> n % 2 == 0
{
   if n == 0 then true else odd(n-1)
}
 
predicate method odd(n: nat)
   ensures odd(n) <==> n % 2 != 0
{
   if n == 0 then false else even(n-1)
}
 
function power(x:int, n:int):int
{
  if n <= 0 then 1
  else x * power(x, n-1)
}

Dafny Matrix Mutiplication

So, I spent quite a while helping someone on stackoverflow prove the correctness of a matrix multiplication algorithm. Once we got to a point where they were happy with it and thanked me, then they deleted their question. I take this, and the fact that in hindsight their understanding did not seem to match up with the code they had, to mean that they were cheating on some university coursework. It took me quite a lot of effort to write the answer, and I wasn’t doing it primarily to help them specificaly, I was doing it to help Dafny become more popular. By which I mean: it was only worth the effort of writing such a detailed answer if the answer can help many other people.

Unfortunately, I don’t have a copy of the answer I wrote. But I do I have a copy of all the code. So here it is. If you are a lecturer and this is your coursework question then I can be contacted on the “about” page.

First the question:

http://rise4fun.com/Dafny/Bztr

method Main()
{
	var m1: array2<int>, m2: array2<int>, m3: array2<int>;
	m1 := new int[2,3];
	m2 := new int[3,1];
	m1[0,0] := 1; m1[0,1] := 2; m1[0,2] := 3;
	m1[1,0] := 4; m1[1,1] := 5; m1[1,2] := 6;
	m2[0,0] := 7;
	m2[1,0] := 8;
	m2[2,0] := 9;
	m3 := Multiply'(m1, m2);
	PrintMatrix(m1);
	print "\n*\n";
	PrintMatrix(m2);
	print "\n=\n";
	PrintMatrix(m3);
}
 
method PrintMatrix(m: array2<int>)
	requires m != null
{
	var i: nat := 0;
	while (i < m.Length0)
	{
		var j: nat := 0;
		print "\n";
		while (j < m.Length1)
		{
			print m[i,j];
			print "\t";
			j := j + 1;
		} 
		i := i + 1;
	} 
	print "\n";
}
predicate MM(m1: array2<int>, m2: array2<int>, m3: array2<int>)
{ // m3 is the result of multiplying the matrix m1 by the matrix m2
	m1 != null && m2 != null && m3 != null &&
	m1.Length1 == m2.Length0 && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 &&
	forall i,j :: 0 <= i < m3.Length0 && 0 <= j < m3.Length1 ==> m3[i,j] == RowColumnProduct(m1,m2,i,j)
}
 
function RowColumnProduct(m1: array2<int>, m2: array2<int>, row: nat, column: nat): int
	requires m1 != null && m2 != null && m1.Length1 == m2.Length0
	requires row < m1.Length0 && column < m2.Length1 
{
	RowColumnProductFrom(m1, m2, row, column, 0)
}
 
function RowColumnProductFrom(m1: array2<int>, m2: array2<int>, row: nat, column: nat, k: nat): int
	requires m1 != null && m2 != null && k <= m1.Length1 == m2.Length0
	requires row < m1.Length0 && column < m2.Length1
	decreases m1.Length1 - k
{
	if k == m1.Length1 then 0 else m1[row,k]*m2[k,column] + RowColumnProductFrom(m1, m2, row, column, k+1)
}
 
function RowColumnProductTo(m1: array2<int>, m2: array2<int>, row: nat, column: nat, k: nat,i:nat): int
	requires m1 != null && m2 != null && k <= m1.Length1 == m2.Length0
	requires row < m1.Length0 && column < m2.Length1 && i < m1.Length1 == m2.Length0
  requires k<=i
	decreases i - k
{
	if k == i then 0 else m1[row,k]*m2[k,column] + RowColumnProductTo(m1, m2, row, column, k+1,i)
}
 
predicate MMROW(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,col:nat)
{ // m3 is the result of multiplying the matrix m1 by the matrix m2
	m1 != null && m2 != null && m3 != null &&
	m1.Length1 == m2.Length0 && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 &&
  row <= m1.Length0 && col <= m2.Length1 &&
	forall i,j :: 0 <= i < row && 0 <= j < col ==> m3[i,j] == RowColumnProduct(m1,m2,i,j)
 
}
 
predicate MMCOL(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,col:nat)
{ // m3 is the result of multiplying the matrix m1 by the matrix m2
	m1 != null && m2 != null && m3 != null &&
	m1.Length1 == m2.Length0 && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 &&
  row <= m1.Length0 && col <= m2.Length1 &&
	forall i,j :: 0 <= i < row && 0 <= j < col ==> m3[i,j] == RowColumnProduct(m1,m2,i,j)
 
}
predicate MMI(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,col:nat,i:nat)
{ // m3 is the result of multiplying the matrix m1 by the matrix m2
	m1 != null && m2 != null && m3 != null &&
	m1.Length1 == m2.Length0 && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 &&
  row < m1.Length0 && col < m2.Length1 && 0<=i<m1.Length1 &&
	forall n,j :: 0 <= n < row && 0 <= j < col ==> m3[n,j] == RowColumnProduct(m1,m2,n,j)
  && m3[row,col] == RowColumnProductTo(m1, m2, row, col ,0,i)
}
 
method Multiply'(m1: array2<int>, m2: array2<int>) returns (m3: array2<int>)
	requires m1 != null && m2 != null
  requires m1.Length1 > 0 && m2.Length0 > 0
	requires m1.Length1 == m2.Length0
	ensures MM(m1, m2, m3)
{
	m3 := new int[m1.Length0, m2.Length1];
  var row:nat := 0;
  var col:nat  := 0;
  var i:nat  := 0;
 
  while(row != m1.Length0)
    invariant MMROW(m1, m2, m3,row, col)
    invariant (0<=row<= m1.Length0)
		decreases m1.Length0 - row
  {
      while(col != m2.Length1)
      invariant MMCOL(m1, m2, m3,row, col)
      invariant (0<=col<= m2.Length1)
  		decreases m2.Length1 - col
      {
          while(i != m1.Length1)
            invariant MMI(m1, m2, m3,row, col,i)
            invariant (i<= m1.Length1==m2.Length0)&&(0<=col<= m2.Length1)&&(0<=row<= m1.Length0)
    		    decreases m1.Length1 - i
           {   
             m3[row,col]:= m3[row,col]+(m1[row,i]*m2[i,col]);
             i := i+1;
           }
           col := col+1;
           i := 0;
      }
      row := row+1;
      col:= 0;
  }
}

Now several different solutions.

The questioners insisted that I not change their definition of the main MM predicate, even though the direction of recursion in the predicate is opposite to the direction of recursion in the while loop. The proof strategy I showed them was to define a new predicate that did recurse in he same direction as the while loop, and then prove the equivalence of the two predicates.

http://rise4fun.com/Dafny/noVy

method Main()
{
    var m1: array2<int>, m2: array2<int>, m3: array2<int>;
    m1 := new int[2,3];
    m2 := new int[3,1];
    m1[0,0] := 1; m1[0,1] := 2; m1[0,2] := 3;
    m1[1,0] := 4; m1[1,1] := 5; m1[1,2] := 6;
    m2[0,0] := 7;
    m2[1,0] := 8;
    m2[2,0] := 9;
    m3 := Multiply'(m1, m2);
    PrintMatrix(m1);
    print "\n*\n";
    PrintMatrix(m2);
    print "\n=\n";
    PrintMatrix(m3);
}
 
method PrintMatrix(m: array2<int>)
    requires m != null
{
    var i: nat := 0;
    while (i < m.Length0)
    {
        var j: nat := 0;
        print "\n";
        while (j < m.Length1)
        {
            print m[i,j];
            print "\t";
            j := j + 1;
        } 
        i := i + 1;
    } 
    print "\n";
}
 
predicate AllowedToMultiply(m1: array2<int>, m2: array2<int>) {
  m1 != null && m2 != null && m1.Length1 == m2.Length0 
}
 
predicate AllowedToMultiplyInto(m1: array2<int>, m2: array2<int>, m3: array2<int>) {
  AllowedToMultiply(m1,m2) && 
  m3 != null && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 
}
 
predicate MM(m1: array2<int>, m2: array2<int>, m3: array2<int>)
{ // m3 is the result of multiplying the matrix m1 by the matrix m2
    AllowedToMultiplyInto(m1,m2,m3) &&
    forall i,j :: 0 <= i < m3.Length0 && 0 <= j < m3.Length1 ==> m3[i,j] == RowColumnProduct(m1,m2,i,j)
}
 
function RowColumnProduct(m1: array2<int>, m2: array2<int>, row: nat, column: nat): int
    requires AllowedToMultiply(m1,m2)
    requires row < m1.Length0 && column < m2.Length1 
{
    RowColumnProductFrom(m1, m2, row, column, 0)
}
 
function RowColumnProductFrom(m1: array2<int>, m2: array2<int>, row: nat, column: nat, k: nat): int
    requires AllowedToMultiply(m1,m2)
    requires row < m1.Length0 && column < m2.Length1
    requires k <= m1.Length1
    decreases m1.Length1 - k
{
    if k == m1.Length1 then 0 else m1[row,k]*m2[k,column] + RowColumnProductFrom(m1, m2, row, column, k+1)
}
 
function RowColumnProductTo(m1: array2<int>, m2: array2<int>, row: nat, column: nat, k: nat,i:nat): int
    requires AllowedToMultiply(m1,m2)
    requires row < m1.Length0 && column < m2.Length1 && i < m1.Length1 == m2.Length0
    requires k<=i
    decreases i - k
{
    if k == i then 0 else m1[row,k]*m2[k,column] + RowColumnProductTo(m1, m2, row, column, k+1,i)
}
 
function RowColumnProductForCount(m1: array2<int>, m2: array2<int>, row: nat, column: nat, n:nat): int
    requires AllowedToMultiply(m1, m2)
    requires row < m1.Length0 && column < m2.Length1 && n <= m1.Length1
{
  if n == 0 then 0 else
    RowColumnProductForCount(m1, m2, row, column, n-1) + m1[row,n-1]*m2[n-1,column] 
}
 
predicate MMROW(m1: array2<int>, m2: array2<int>, m3: array2<int>, rown:nat)
  requires AllowedToMultiplyInto(m1, m2, m3)
  requires rown <= m1.Length0 
{ 
    forall r:nat,c:nat :: r < rown && c < m2.Length1 ==> m3[r,c] == RowColumnProductForCount(m1,m2,r,c,m1.Length1) 
}
 
predicate MMCOL(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,coln:nat)
  requires AllowedToMultiplyInto(m1, m2, m3)
  requires row < m1.Length0 && coln <= m2.Length1  
{ 
    forall c:nat :: c < coln ==> m3[row,c] == RowColumnProductForCount(m1,m2,row,c,m1.Length1)
}
 
predicate MMI(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,col:nat,n:nat)
   requires AllowedToMultiplyInto(m1, m2, m3)
   requires row < m1.Length0 && col < m2.Length1 && n<=m1.Length1
{ 
   m3[row,col] == RowColumnProductForCount(m1, m2, row, col, n)
}
 
method Multiply'(m1: array2<int>, m2: array2<int>) returns (m3: array2<int>)
    requires AllowedToMultiply(m1, m2)
    ensures MM(m1, m2, m3)
{
    m3 := new int[m1.Length0, m2.Length1];
 
  var row:nat := 0;
  // loop over rows of m1
  while(row < m1.Length0)
    invariant row <= m1.Length0
    invariant forall rn:nat :: rn <= row ==> MMROW(m1, m2, m3, rn)
    modifies m3
  {
      assert MMROW(m1, m2, m3, row);
      // loop over coloums of m2
      var col:nat  := 0;
      while(col < m2.Length1)
        invariant col <= m2.Length1
        invariant forall rn:nat :: rn <= row ==> MMROW(m1, m2, m3, rn)
        invariant forall n:nat :: n <= col ==> MMCOL(m1, m2, m3,row, n)
        {
          assert MMCOL(m1, m2, m3, row, col); //
          // loop over elements of m1 row / m2 column
          var i:nat  := 0;
          m3[row,col] := 0;
          while(i < m1.Length1)
            invariant i <= m1.Length1
            invariant forall rn:nat :: rn < row ==> MMROW(m1, m2, m3, rn)
            invariant forall c:nat :: c < col ==> MMCOL(m1, m2, m3, row, c)
            invariant forall j:nat :: j <= i ==> MMI(m1, m2, m3, row, col, j)
           { 
             assert MMI(m1, m2, m3, row, col, i);
 
             m3[row,col]:= m3[row,col]+(m1[row,i]*m2[i,col]);
             i := i+1;
 
             assert MMI(m1, m2, m3, row, col, i);
           }
           assert MMI(m1, m2, m3, row, col, m1.Length1);
           assert m3[row,col] == RowColumnProductForCount(m1,m2,row,col,m1.Length1);
           col := col+1;
           assert MMCOL(m1, m2, m3, row, col);
        }
      assert MMCOL(m1, m2, m3, row, m2.Length1);
      row := row+1;
      assert MMROW(m1, m2, m3, row);
  }
  assert MMROW(m1, m2, m3, m1.Length0);
  MMROWImpliesMM(m1, m2, m3);
}
 
lemma MMROWImpliesMM(m1: array2<int>, m2: array2<int>, m3: array2<int>)
   requires AllowedToMultiplyInto(m1,m2,m3)
   requires MMROW(m1, m2, m3, m1.Length0)
   ensures MM(m1, m2, m3)
{
    assert forall r:nat,c:nat :: r < m1.Length0 && c < m2.Length1 ==> m3[r,c] == RowColumnProductForCount(m1,m2,r,c,m1.Length1);
 
    forall r:nat,c:nat | r < m1.Length0 && c < m2.Length1
      ensures m3[r,c] == RowColumnProduct(m1,m2,r,c)
    {
      assert m3[r,c] == RowColumnProductForCount(m1,m2,r,c,m1.Length1);
      RowColumnProductForCountImpliesRowColumnProduct(m1, m2, m3, r, c);  
    }
 
    assert forall r:nat,c:nat :: r < m3.Length0 && c < m3.Length1 ==> m3[r,c] == RowColumnProduct(m1,m2,r,c);  
}   
 
lemma RowColumnProductForCountImpliesRowColumnProduct(m1: array2<int>, m2: array2<int>, m3: array2<int>, r:nat, c:nat)
   requires AllowedToMultiplyInto(m1,m2,m3)
   requires r < m1.Length0 && c < m2.Length1;
   requires m3[r,c] == RowColumnProductForCount(m1,m2,r,c,m1.Length1)
   ensures m3[r,c] == RowColumnProduct(m1,m2,r,c)
{
  assert RowColumnProduct(m1,m2,r,c) == RowColumnProductFrom(m1,m2,r,c,0);
 
  var i:nat := 0;
  var total := RowColumnProductForCount(m1,m2,r,c,m1.Length1);
  while i < m1.Length1
     invariant i <= m1.Length1
     invariant total == RowColumnProductForCount(m1,m2,r,c,m1.Length1-i) + RowColumnProductFrom(m1,m2,r,c,m1.Length1-i)
  {
    i := i+1;
  }
}

I suggested an alternative strategy which uses Dafny’s forall statement to implement the matrix multiplication. Since this is not a loop it does not require any invariants to be given in order to verify. This is the best solution if you are just trying to get a matrix multiply working.

http://rise4fun.com/Dafny/mgoeu

method Main()
{
	var m1: array2<int>, m2: array2<int>, m3: array2<int>;
	m1 := new int[2,3];
	m2 := new int[3,1];
	m1[0,0] := 1; m1[0,1] := 2; m1[0,2] := 3;
	m1[1,0] := 4; m1[1,1] := 5; m1[1,2] := 6;
	m2[0,0] := 7;
	m2[1,0] := 8;
	m2[2,0] := 9;
	m3 := Multiply'(m1, m2);
	PrintMatrix(m1);
	print "\n*\n";
	PrintMatrix(m2);
	print "\n=\n";
	PrintMatrix(m3);
}
 
method PrintMatrix(m: array2<int>)
	requires m != null
{
	var i: nat := 0;
	while (i < m.Length0)
	{
		var j: nat := 0;
		print "\n";
		while (j < m.Length1)
		{
			print m[i,j];
			print "\t";
			j := j + 1;
		} 
		i := i + 1;
	} 
	print "\n";
}
 
predicate AllowedToMultiply(m1: array2<int>, m2: array2<int>) {
  m1 != null && m2 != null && m1.Length1 == m2.Length0 
}
 
predicate MM(m1: array2<int>, m2: array2<int>, m3: array2<int>)
  requires AllowedToMultiply(m1, m2)
{ // m3 is the result of multiplying the matrix m1 by the matrix m2
  m3 != null && 
  m3.Length0 == m1.Length0 && 
  m3.Length1 == m2.Length1 &&
	forall r:nat,c:nat :: r < m3.Length0 && c < m3.Length1 ==> 
    m3[r,c] == RowColumnProductTo(m1,m2,r,c,m1.Length1) 
}
 
function method RowColumnProductTo(m1: array2<int>, m2: array2<int>, row: nat, column: nat, n:nat): int
	requires AllowedToMultiply(m1, m2)
	requires row < m1.Length0 && column < m2.Length1 && n <= m1.Length1
{
  if n == 0 then 0 else
    RowColumnProductTo(m1, m2, row, column, n-1) + m1[row,n-1]*m2[n-1,column] 
}
 
method Multiply'(m1: array2<int>, m2: array2<int>) returns (m3: array2<int>)
	requires AllowedToMultiply(m1, m2)
	ensures MM(m1, m2, m3)
{
	m3 := new int[m1.Length0, m2.Length1];
 
  forall r:nat,c:nat | r < m3.Length0 && c < m3.Length1
  {
     m3[r,c] := RowColumnProductTo(m1,m2,r,c,m1.Length1);
  }
}

In this version I take the approach of changing the definition of the MM predicate to work in the same direction as the iteration. If you don’t want to go down the route of using the forall statement, then in my opinion it is usually most productive if you get your recursive and iterative definitions to bracket the same way. For example, have them both do ((((a+b)+c)+d)+e), don’t have one of the do (a+(b+(c+(d+e)))).

method Main()
{
	var m1: array2<int>, m2: array2<int>, m3: array2<int>;
	m1 := new int[2,3];
	m2 := new int[3,1];
	m1[0,0] := 1; m1[0,1] := 2; m1[0,2] := 3;
	m1[1,0] := 4; m1[1,1] := 5; m1[1,2] := 6;
	m2[0,0] := 7;
	m2[1,0] := 8;
	m2[2,0] := 9;
	m3 := Multiply'(m1, m2);
	PrintMatrix(m1);
	print "\n*\n";
	PrintMatrix(m2);
	print "\n=\n";
	PrintMatrix(m3);
}
 
method PrintMatrix(m: array2<int>)
	requires m != null
{
	var i: nat := 0;
	while (i < m.Length0)
	{
		var j: nat := 0;
		print "\n";
		while (j < m.Length1)
		{
			print m[i,j];
			print "\t";
			j := j + 1;
		} 
		i := i + 1;
	} 
	print "\n";
}
 
predicate AllowedToMultiply(m1: array2<int>, m2: array2<int>) {
  m1 != null && m2 != null && m1.Length1 == m2.Length0 
}
 
predicate AllowedToMultiplyInto(m1: array2<int>, m2: array2<int>, m3: array2<int>) {
  AllowedToMultiply(m1,m2) && 
  m3 != null && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 
}
 
predicate MM(m1: array2<int>, m2: array2<int>, m3: array2<int>)
  requires AllowedToMultiply(m1, m2)
{ // m3 is the result of multiplying the matrix m1 by the matrix m2
  m3 != null && 
  m3.Length0 == m1.Length0 && 
  m3.Length1 == m2.Length1 &&
	forall r:nat,c:nat :: r < m3.Length0 && c < m3.Length1 ==> 
    m3[r,c] == RowColumnProductTo(m1,m2,r,c,m1.Length1) 
}
 
function RowColumnProductTo(m1: array2<int>, m2: array2<int>, row: nat, column: nat, n:nat): int
	requires AllowedToMultiply(m1, m2)
	requires row < m1.Length0 && column < m2.Length1 && n <= m1.Length1
{
  if n == 0 then 0 else
    RowColumnProductTo(m1, m2, row, column, n-1) + m1[row,n-1]*m2[n-1,column] 
}
 
predicate MMROW(m1: array2<int>, m2: array2<int>, m3: array2<int>, rown:nat)
  requires AllowedToMultiplyInto(m1, m2, m3)
  requires rown <= m1.Length0 
{ 
	forall r:nat,c:nat :: r < rown && c < m2.Length1 ==> m3[r,c] == RowColumnProductTo(m1,m2,r,c,m1.Length1) 
}
 
predicate MMCOL(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,coln:nat)
  requires AllowedToMultiplyInto(m1, m2, m3)
  requires row < m1.Length0 && coln <= m2.Length1  
{ 
	forall c:nat :: c < coln ==> m3[row,c] == RowColumnProductTo(m1,m2,row,c,m1.Length1)
}
 
predicate MMI(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,col:nat,n:nat)
   requires AllowedToMultiplyInto(m1, m2, m3)
   requires row < m1.Length0 && col < m2.Length1 && n<=m1.Length1
{ 
   m3[row,col] == RowColumnProductTo(m1, m2, row, col, n)
}
 
method Multiply'(m1: array2<int>, m2: array2<int>) returns (m3: array2<int>)
	requires AllowedToMultiply(m1, m2)
	ensures MM(m1, m2, m3)
{
	m3 := new int[m1.Length0, m2.Length1];
 
  var row:nat := 0;
  // loop over rows of m1
  while(row < m1.Length0)
    invariant row <= m1.Length0
    invariant forall rn:nat :: rn <= row ==> MMROW(m1, m2, m3, rn)
    modifies m3
  {
      assert MMROW(m1, m2, m3, row);
      // loop over coloums of m2
      var col:nat  := 0;
      while(col < m2.Length1)
        invariant col <= m2.Length1
        invariant forall rn:nat :: rn <= row ==> MMROW(m1, m2, m3, rn)
        invariant forall n:nat :: n <= col ==> MMCOL(m1, m2, m3,row, n)
        {
          assert MMCOL(m1, m2, m3, row, col); //
          // loop over elements of m1 row / m2 column
          var i:nat  := 0;
          m3[row,col] := 0;
          while(i < m1.Length1)
            invariant i <= m1.Length1
            invariant forall rn:nat :: rn < row ==> MMROW(m1, m2, m3, rn)
            invariant forall c:nat :: c < col ==> MMCOL(m1, m2, m3, row, c)
            invariant forall j:nat :: j <= i ==> MMI(m1, m2, m3, row, col, j)
           { 
             assert MMI(m1, m2, m3, row, col, i);
 
             m3[row,col]:= m3[row,col]+(m1[row,i]*m2[i,col]);
             i := i+1;
 
             assert MMI(m1, m2, m3, row, col, i);
           }
           assert MMI(m1, m2, m3, row, col, m1.Length1);
           assert m3[row,col] == RowColumnProductTo(m1,m2,row,col,m1.Length1);
           col := col+1;
           assert MMCOL(m1, m2, m3, row, col);
        }
      assert MMCOL(m1, m2, m3, row, m2.Length1);
      row := row+1;
      assert MMROW(m1, m2, m3, row);
  }
  assert MMROW(m1, m2, m3, m1.Length0);
}

Here are various other intermidiate stages and suggestions. We went through quite a few iterations, because their requirements on what I could and couldn’t change were not intuiative. I now presume that was because they didn’t want to say to me “here is the coursework specification, look it says don’t change that bit”.

In fact, looking in more detail, one of the attempts that they shared with me has this comment in it

// TODO: continue here, multiplying m1 by m2 placing the result in m3 such that MM(m1, m2, m3) will become true

Which looks to me just like the kind of thing that I have seen written in many other courseworks. Hmm. Sucks.

http://rise4fun.com/Dafny/5F2R2
http://rise4fun.com/Dafny/6PNo
http://rise4fun.com/Dafny/mXi49
http://rise4fun.com/Dafny/VtXb
http://rise4fun.com/Dafny/mgoeu
http://rise4fun.com/Dafny/1Yslx
http://rise4fun.com/Dafny/WUop
http://rise4fun.com/Dafny/RPnU
http://rise4fun.com/Dafny/ji9A

Calculations In Dafny

Here is an example of using calc in Dafny.

Notes:

  • Instead of using ==, you can write another relational operator, for example implication ==>
  • I set the Add function to opaque, and disabled automatic induction, because otherwise Dafny will prove almost all of these lemmas automatically
  • I wrote in the decreases clauses for didactic reasons. I wrote decreases 0 where there is no recursive call
  • I got the idea for this example from this document by Sophia Drossopoulou
datatype Num = Zero | Succ(pred:Num)
 
function {:opaque true} Add(x:Num, y:Num) : Num
    decreases x;
{
    match x {
        case Zero => y
        case Succ(z) => Succ(Add(z, y))
    }
}
 
lemma {:induction false} ZeroIdentity(x:Num)
   decreases x;
   ensures Add(x,Zero) == x
{
    match x {
        case Zero =>
            calc == {
                Add(Zero,Zero);
                    {reveal_Add();}
                Zero;
            }
        case Succ(z) =>
            calc == {
                Add(x,Zero);
                    {reveal_Add();}
                Succ(Add(z,Zero));
                    {ZeroIdentity(z);}
                Succ(z);
                    // definition of Num
                x;
            }
    }
}
 
lemma {:induction false} SuccSymmetry(x:Num, y:Num)
    decreases 0;
    ensures Add(Succ(x),y) == Add(x,Succ(y))
{
    calc == {
        Add(Succ(x),y);
            {reveal_Add();}
        Succ(Add(x,y));
            {SuccLemmaFour(x, y);}
        Add(x,Succ(y));
    }
}
 
lemma {:induction false} SuccLemmaFour(x:Num, y:Num)
    decreases x;
    ensures Succ(Add(x, y)) == Add(x,Succ(y));
{
    match x {
        case Zero =>
            calc == {
                Succ(Add(Zero, y));
                    {reveal_Add();}
                Succ(y);
                    {reveal_Add();}
                Add(Zero,Succ(y));
            }
        case Succ(z) =>
            calc == {
                Succ(Add(x, y));
                    {reveal_Add();}
                Succ(Succ(Add(z, y)));
                    {SuccLemmaFour(z, y);}
                Succ(Add(z, Succ(y)));
                    {reveal_Add();}
                Add(x,Succ(y));
            }
    }
}
 
lemma {:induction false} AddCommutative(x:Num, y:Num)
    decreases x;
    ensures Add(x, y) == Add(y, x)
{
    match x {
        case Zero =>
            calc == {
                Add(Zero, y);
                    {reveal_Add();}
                y;
                    {ZeroIdentity(y);}
                Add(y, Zero);
            }
        case Succ(z) =>
            calc == {
                Add(x, y);
                    {reveal_Add();}
                Succ(Add(z, y));
                    {AddCommutative(z, y);}
                Succ(Add(y, z));
                    {SuccLemmaFour(y, z);}
                Add(y,Succ(z));
                    // definition Num 
                Add(y, x);
            }
    }
}
 
lemma {:induction false} AddAssociative(x:Num, y:Num, z:Num)
    decreases x;
    ensures Add(Add(x,y),z) == Add(x,Add(y,z));
{
    match x {
        case Zero =>
            calc == {
                Add(Add(Zero,y),z);
                    {reveal_Add();}
                Add(y,z);
                    {reveal_Add();}
                Add(Zero,Add(y,z));
            }
        case Succ(w) =>
            calc == {
                Add(Add(x,y),z);
                    {reveal_Add();}
                Add(Add(Succ(w),y),z);
                    {SuccSymmetry(w,y);}
                Add(Add(w,Succ(y)),z);
                    {SuccLemmaFour(w, y);}
                Add(Succ(Add(w,y)),z);
                    {SuccSymmetry(Add(w,y),z);}
                Add(Add(w,y),Succ(z));
                    {SuccLemmaFour(Add(w,y), z);}
                Succ(Add(Add(w,y),z));
                    {AddAssociative(w,y,z);}
                Succ(Add(w,Add(y,z)));
                    {SuccLemmaFour(w, Add(y,z));}
                Add(w,Succ(Add(y,z)));
                    {SuccSymmetry(w,Add(y,z));}
                Add(Succ(w),Add(y,z));
                    {reveal_Add();}
                Add(x,Add(y,z));
            }
    }
}

Dafny Sum and Max solution

A Dafny solution to the Sum and Max verification benchmark. I added some additional specification to verify that the result max is really the maximum and the sum is really the sum.

method SumMax(a: array<int>) returns (sum:int, max:int)
 requires a != null;
 requires a.Length >= 0;
 requires forall i :: 0 <= i < a.Length ==> a[i] >= 0;
 ensures sum <= a.Length*max;
 ensures forall i :: 0 <= i < a.Length ==> a[i] <= max;
 ensures a.Length == 0 || 
         (exists i :: 0 <= i < a.Length && a[i] == max);
 ensures sum == Sum(a);
{
 max := 0;
 sum := 0;
 
 var idx:int := 0;
 while idx<a.Length 
  invariant idx <= a.Length;
  invariant forall i :: 0 <= i < idx ==> a[i] <= max;
  invariant (idx==0 && max==0) || 
            exists i :: 0 <= i < idx && a[i] == max;
  invariant sum <= idx*max;
  invariant sum == Sum'(a, 0, idx);
 {
  if (max < a[idx])
  {
   max := a[idx];
  }
  sum := sum + a[idx];
  idx := idx + 1;
 }
}
 
function Sum(a: array<int>) : int
 reads a;
 requires a != null;
{
 Sum'(a, 0, a.Length)
}
 
function Sum'(a: array<int>, i:int, j:int) : int
 reads a;
 requires a != null;
 requires 0 <= i <= j <= a.Length;
{
 if j == i then 0 else Sum'(a, i, j-1) + a[j-1]
}
 
lemma SumOfIntervalOneIsElement(a: array<int>, i:int)
 requires a != null;
 requires 0 <= i < a.Length;
 ensures a.Length > 0;
 ensures Sum'(a, i, i+1) == a[i];
{ }
 
lemma SumOfIntervalIsSumOfSubIntervals
  (a: array<int>, i:int, j:int, k:int)
 requires a != null;
 requires 0 <= i <= j <= k <= a.Length;
 ensures Sum'(a, i, j) + Sum'(a, j, k) == Sum'(a, i, k);
{ }