Importing Daml Contracts in Daml Studio

Is there a way that if I have a DAML Contract and I want to import it or directly run on DAML Studio?

I’m not sure what you mean by “if I have a Daml Contract”. A Daml contract is a value written to a ledger, an instance of a template. I like the analogy that a contract is a bit like an object, and a template like a class in object-oriented programming, though not everyone likes that analogy.

Whenever you come a cross a contract (via the Ledger API or in Daml Studio), you can also get your hands on the Daml package that defined the template. You can import that package in a Daml project in Daml Studio using data-dependencies, and then instantiate the contract in a Daml Script.

This may be a bit abstract. If you could be a bit more specific about what you are trying to achieve, I could probably provide specific steps.

I am working on Smart Contract Modelling and verification. What I want is that once I verified the DAML Contract using formal verification method then how I can run the verified DAML Contract on DAML Studio? via any API or what.

You can run contracts you’ve written in Daml Studio directly in Daml studio on an in-memory test ledger using Daml Script.
The same script can then also be executed against a production ledger.

How I can write a daml script for this example:

module User where

-- MAIN_TEMPLATE_BEGIN

template User with

    username: Party

    following: [Party]

  where

    signatory username

    observer following

-- MAIN_TEMPLATE_END

    key username: Party

    maintainer key

    -- FOLLOW_BEGIN

    nonconsuming choice Follow: ContractId User with

        userToFollow: Party

      controller username

      do

        assertMsg "You cannot follow yourself" (userToFollow /= username)

        assertMsg "You cannot follow the same user twice" (notElem userToFollow following)

        archive self

        create this with following = userToFollow :: following

    -- FOLLOW_END

Here is a simple example:

module User where

import Daml.Script

template User with
    username: Party
    following: [Party]
  where
    signatory username
    observer following
    key username: Party
    maintainer key
    nonconsuming choice Follow: ContractId User with
        userToFollow: Party
      controller username
      do
        assertMsg "You cannot follow yourself" (userToFollow /= username)
        assertMsg "You cannot follow the same user twice" (notElem userToFollow following)
        archive self
        create this with following = userToFollow :: following

test = script do
  alice <- allocateParty "Alice"
  bob <- allocateParty "Bob"
  aliceUser <- submit alice $ createCmd User with username = alice, following = []
  bobUser <- submit bob $ createCmd User with username = bob, following = []
  submit alice $ exerciseCmd aliceUser (Follow bob)
  pure ()

I recommend taking a look at the documentation for more details and an explanation of the functions in this script.

There’s a whole interactive tutorial dedicated to writing a script for the User example. Take a look at this: Learn Damlsmart contract Language - Interactive Learning Tutorials